Certificate for #19693 ⟨a, b | aba=a, babab=bb⟩

Back:⟨a, b | aba=a, babab=bb⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #1.

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

[2] bab=bb

Axiom: babab=bb.

Reduce LHS:

[1]b(aba)b
⇒ bab

Defines rule #3.

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

[3] abb=ab

Overlap of [1] aba=a with [2] bab=bb:

a ba bab

Critical pair: abb=ab.

Defines rule #2.

Referenced by [5].

[4] bba=ba

Overlap of [2] bab=bb with [1] aba=a:

b ab aba

Critical pair: ba=bba.

Flip LHS and RHS.

Defines rule #4.

[5] bbb=bb

Overlap of [2] bab=bb with [3] abb=ab:

b ab abb

Critical pair: bab=bbb.

Reduce LHS:

[2](bab)
⇒ bb

Flip LHS and RHS.

Defines rule #5.