Certificate for #16239 ⟨a, b | aab=ba, abbb=ba⟩

Back:⟨a, b | aab=ba, abbb=ba⟩

Completion settings:

[1] aab=ba

Axiom: aab=ba.

Referenced by [3].

[2] ba=abbb

Axiom: abbb=ba.

Flip LHS and RHS.

Defines rule #2.

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

[3] aab=abbb

Simplify [1] aab=ba.

Reduce RHS:

[2](ba)
⇒ abbb

Defines rule #3.

Referenced by [4], [5].

[4] abbbbbbbbbbb=abbbbbbb

Overlap of [3] aab=abbb with [2] ba=abbb:

aa b ba

Critical pair: aaabbb=abbba.

Reduce LHS:

[3]a(aab)bb
[3]⇒ (aab)bbbb
⇒ abbbbbbb

Reduce RHS:

[2]abb(ba)
[2]⇒ ab(ba)bbb
[2]⇒ a(ba)bbbbbb
[3]⇒ (aab)bbbbbbbb
⇒ abbbbbbbbbbb

Flip LHS and RHS.

Referenced by [5].

[5] abbbbbbbb=abbbbbb

Overlap of [2] ba=abbb with [3] aab=abbb:

b a aab

Critical pair: babbb=abbbab.

Reduce LHS:

[2](ba)bbb
⇒ abbbbbb

Reduce RHS:

[2]abb(ba)b
[2]⇒ ab(ba)bbbb
[2]⇒ a(ba)bbbbbbb
[3]⇒ (aab)bbbbbbbbb
[4]⇒ (abbbbbbbbbbb)b
⇒ abbbbbbbb

Flip LHS and RHS.

Defines rule #1.