Certificate for #19546 ⟨a, b | aab=b, ababa=ba⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

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

[2] ababa=ba

Axiom: ababa=ba.

Referenced by [3], [4].

[3] baba=aba

Overlap of [1] aab=b with [2] ababa=ba:

a ab ababa

Critical pair: aba=baba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [7].

[4] abba=aba

Overlap of [2] ababa=ba with [2] ababa=ba:

ab aba ababa

Critical pair: abba=baba.

Reduce RHS:

[3](baba)
⇒ aba

Referenced by [5].

[5] bba=ba

Overlap of [1] aab=b with [4] abba=aba:

a ab abba

Critical pair: aaba=bba.

Reduce LHS:

[1](aab)a
⇒ ba

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] bbb=bb

Overlap of [5] bba=ba with [1] aab=b:

bb a aab

Critical pair: bbb=baab.

Reduce RHS:

[1]b(aab)
⇒ bb

Defines rule #3.

[7] babb=abb

Overlap of [3] baba=aba with [1] aab=b:

bab a aab

Critical pair: babb=abaab.

Reduce RHS:

[1]ab(aab)
⇒ abb

Defines rule #5.