Certificate for #7142 ⟨a, b | bb=aa, aaab=ab⟩

Back:⟨a, b | bb=aa, aaab=ab⟩

Completion settings:

[1] aa=bb

Axiom: bb=aa.

Flip LHS and RHS.

Defines rule #1.

Referenced by [2], [3], [5].

[2] bbab=ab

Axiom: aaab=ab.

Reduce LHS:

[1](aa)ab
⇒ bbab

Defines rule #3.

Referenced by [4], [5].

[3] abb=bba

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

a a aa

Critical pair: abb=bba.

Defines rule #2.

Referenced by [4], [5].

[4] bbbba=bba

Overlap of [2] bbab=ab with [3] abb=bba:

bb ab abb

Critical pair: bbbba=abb.

Reduce RHS:

[3](abb)
⇒ bba

Defines rule #5.

[5] bbbbb=bbb

Overlap of [3] abb=bba with [2] bbab=ab:

a bb bbab

Critical pair: aab=bbaab.

Reduce LHS:

[1](aa)b
⇒ bbb

Reduce RHS:

[1]bb(aa)b
⇒ bbbbb

Flip LHS and RHS.

Defines rule #4.