Certificate for #3519 ⟨a, b | aa=1, abbba=bb⟩

Back:⟨a, b | aa=1, abbba=bb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #4.

Referenced by [3], [4], [8].

[2] abbba=bb

Axiom: abbba=bb.

Referenced by [3], [4], [6].

[3] bbba=abb

Overlap of [1] aa=1 with [2] abbba=bb:

a a abbba

Critical pair: abb=bbba.

Flip LHS and RHS.

Referenced by [5].

[4] bba=abbb

Overlap of [2] abbba=bb with [1] aa=1:

abbb a aa

Critical pair: abbb=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6], [7].

[5] babbb=abb

Simplify [3] bbba=abb.

Reduce LHS:

[4]b(bba)
⇒ babbb

Referenced by [6], [7].

[6] bababb=bb

Overlap of [5] babbb=abb with [4] bba=abbb:

babb b bba

Critical pair: babbabbb=abbba.

Reduce LHS:

[5]bab(babbb)
⇒ bababb

Reduce RHS:

[2](abbba)
⇒ bb

Referenced by [8].

[7] babb=abbbbbb

Overlap of [4] bba=abbb with [5] babbb=abb:

b ba babbb

Critical pair: babb=abbbbbb.

Defines rule #2.

Referenced by [8].

[8] bbbbbbb=bb

Simplify [6] bababb=bb.

Reduce LHS:

[7]ba(babb)
[1]⇒ b(aa)bbbbbb
⇒ bbbbbbb

Defines rule #1.