Certificate for #16167 ⟨a, b | aab=ab, abab=ba⟩

Back:⟨a, b | aab=ab, abab=ba⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Defines rule #1.

Referenced by [3], [4].

[2] abab=ba

Axiom: abab=ba.

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

[3] aba=ba

Overlap of [1] aab=ab with [2] abab=ba:

a ab abab

Critical pair: aba=abab.

Reduce RHS:

[2](abab)
⇒ ba

Defines rule #2.

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

[4] abba=bab

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

ab ab abab

Critical pair: abba=baab.

Reduce RHS:

[1]b(aab)
⇒ bab

Referenced by [6].

[5] bab=ba

Overlap of [2] abab=ba with [3] aba=ba:

abab aba

Critical pair: bab=ba.

Defines rule #4.

Referenced by [6], [7].

[6] baa=ba

Overlap of [2] abab=ba with [3] aba=ba:

ab ab aba

Critical pair: abba=baa.

Reduce LHS:

[4](abba)
[5]⇒ (bab)
⇒ ba

Flip LHS and RHS.

Defines rule #3.

Referenced by [7].

[7] bba=ba

Overlap of [5] bab=ba with [3] aba=ba:

b ab aba

Critical pair: bba=baa.

Reduce RHS:

[6](baa)
⇒ ba

Defines rule #5.