Certificate for #5393 ⟨a, b | aab=ba, aba=bb⟩

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

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [2], [3], [4].

[2] bb=aaab

Axiom: aba=bb.

Reduce LHS:

[1]a(ba)
⇒ aaab

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aaaaaaab=aaaaab

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

b b ba

Critical pair: baab=aaaba.

Reduce LHS:

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

Reduce RHS:

[1]aaa(ba)
⇒ aaaaab

Referenced by [4].

[4] aaaaaab=aaaaab

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

b b bb

Critical pair: baaab=aaabb.

Reduce LHS:

[1](ba)aab
[1]⇒ aa(ba)ab
[1]⇒ aaaa(ba)b
[2]⇒ aaaaaa(bb)
[3]⇒ aa(aaaaaaab)
[3]⇒ (aaaaaaab)
⇒ aaaaab

Reduce RHS:

[2]aaa(bb)
⇒ aaaaaab

Flip LHS and RHS.

Defines rule #1.