Certificate for #15972 ⟨a, b | aaa=aa, baab=ab⟩

Back:⟨a, b | aaa=aa, baab=ab⟩

Completion settings:

[1] aaa=aa

Axiom: aaa=aa.

Defines rule #1.

Referenced by [3].

[2] baab=ab

Axiom: baab=ab.

Referenced by [3], [4].

[3] aab=ab

Overlap of [2] baab=ab with [2] baab=ab:

baa b baab

Critical pair: baaab=abaab.

Reduce LHS:

[1]b(aaa)b
[2]⇒ (baab)
⇒ ab

Reduce RHS:

[2]a(baab)
⇒ aab

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] bab=ab

Overlap of [2] baab=ab with [3] aab=ab:

b aab aab

Critical pair: bab=ab.

Defines rule #3.