Certificate for #5340 ⟨a, b | aaa=bb, aab=ba⟩

Back:⟨a, b | aaa=bb, aab=ba⟩

Completion settings:

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[2] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aaaaaab=aaab

Overlap of [1] bb=aaa with [1] bb=aaa:

b b bb

Critical pair: baaa=aaab.

Reduce LHS:

[2](ba)aa
[2]⇒ aa(ba)a
[2]⇒ aaaa(ba)
⇒ aaaaaab

Defines rule #2.

[4] aaaaaaa=aaaa

Overlap of [1] bb=aaa with [2] ba=aab:

b b ba

Critical pair: baab=aaaa.

Reduce LHS:

[2](ba)ab
[2]⇒ aa(ba)b
[1]⇒ aaaa(bb)
⇒ aaaaaaa

Defines rule #1.