Certificate for #639 ⟨a, b | ab=aa, baa=b⟩

Back:⟨a, b | ab=aa, baa=b⟩

Completion settings:

[1] aa=ab

Axiom: ab=aa.

Flip LHS and RHS.

Defines rule #2.

Referenced by [2], [3].

[2] bab=b

Axiom: baa=b.

Reduce LHS:

[1]b(aa)
⇒ bab

Referenced by [4], [5].

[3] aba=abb

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

a a aa

Critical pair: aab=aba.

Reduce LHS:

[1](aa)b
⇒ abb

Flip LHS and RHS.

Referenced by [4].

[4] ba=bb

Overlap of [2] bab=b with [3] aba=abb:

b ab aba

Critical pair: babb=ba.

Reduce LHS:

[2](bab)b
⇒ bb

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] bbb=b

Overlap of [2] bab=b with [4] ba=bb:

bab ba

Critical pair: bbb=b.

Defines rule #3.