Certificate for #19252 ⟨a, b | aaa=a, aabab=ba⟩

Back:⟨a, b | aaa=a, aabab=ba⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [3], [6].

[2] aabab=ba

Axiom: aabab=ba.

Referenced by [3], [4].

[3] aaba=ba

Overlap of [1] aaa=a with [2] aabab=ba:

aa a aabab

Critical pair: aaba=aabab.

Reduce RHS:

[2](aabab)
⇒ ba

Defines rule #4.

Referenced by [4], [6].

[4] bab=ba

Overlap of [2] aabab=ba with [3] aaba=ba:

aabab aaba

Critical pair: bab=ba.

Defines rule #2.

Referenced by [5].

[5] baab=baa

Overlap of [4] bab=ba with [4] bab=ba:

ba b bab

Critical pair: baba=baab.

Reduce LHS:

[4](bab)a
⇒ baa

Flip LHS and RHS.

Defines rule #5.

Referenced by [6].

[6] bba=ba

Overlap of [5] baab=baa with [3] aaba=ba:

b aab aaba

Critical pair: bba=baaa.

Reduce RHS:

[1]b(aaa)
⇒ ba

Defines rule #3.