Certificate for #16164 ⟨a, b | aab=ab, abaa=bb⟩

Back:⟨a, b | aab=ab, abaa=bb⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Defines rule #1.

Referenced by [3], [4].

[2] bb=abaa

Axiom: abaa=bb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] babaa=abab

Overlap of [2] bb=abaa with [2] bb=abaa:

b b bb

Critical pair: babaa=abaab.

Reduce RHS:

[1]ab(aab)
⇒ abab

Defines rule #3.

Referenced by [4].

[4] babab=abab

Overlap of [2] bb=abaa with [3] babaa=abab:

b b babaa

Critical pair: babab=abaaabaa.

Reduce RHS:

[1]aba(aab)aa
[1]⇒ ab(aab)aa
[3]⇒ a(babaa)
[1]⇒ (aab)ab
⇒ abab

Defines rule #4.