Certificate for #6652 ⟨a, b | aab=a, bbab=ba⟩

Back:⟨a, b | aab=a, bbab=ba⟩

Completion settings:

[1] aab=a

Axiom: aab=a.

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

[2] bbab=ba

Axiom: bbab=ba.

Referenced by [3], [5].

[3] abab=aa

Overlap of [1] aab=a with [2] bbab=ba:

aa b bbab

Critical pair: aaba=abab.

Reduce LHS:

[1](aab)a
⇒ aa

Flip LHS and RHS.

Referenced by [4], [5].

[4] aaa=a

Overlap of [1] aab=a with [3] abab=aa:

a ab abab

Critical pair: aaa=aab.

Reduce RHS:

[1](aab)
⇒ a

Defines rule #2.

Referenced by [6].

[5] bbaa=ba

Overlap of [2] bbab=ba with [3] abab=aa:

bb ab abab

Critical pair: bbaa=baab.

Reduce RHS:

[1]b(aab)
⇒ ba

Referenced by [7].

[6] ab=aa

Overlap of [4] aaa=a with [1] aab=a:

a aa aab

Critical pair: aa=ab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] bba=baa

Overlap of [5] bbaa=ba with [1] aab=a:

bb aa aab

Critical pair: bba=bab.

Reduce RHS:

[6]b(ab)
⇒ baa

Defines rule #3.