Certificate for #16100 ⟨a, b | aab=aa, abaa=bb⟩

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

Completion settings:

[1] aab=aa

Axiom: aab=aa.

Defines rule #2.

Referenced by [3], [4].

[2] bb=abaa

Axiom: abaa=bb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aaaaa=aa

Overlap of [1] aab=aa with [2] bb=abaa:

aa b bb

Critical pair: aaabaa=aab.

Reduce LHS:

[1]a(aab)aa
⇒ aaaaa

Reduce RHS:

[1](aab)
⇒ aa

Defines rule #1.

[4] babaa=abaa

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

b b bb

Critical pair: babaa=abaab.

Reduce RHS:

[1]ab(aab)
⇒ abaa

Defines rule #4.