Certificate for #16069 ⟨a, b | aaa=bb, abbb=ba⟩

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

Completion settings:

[1] aaa=bb

Axiom: aaa=bb.

Defines rule #4.

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

[2] ba=abbb

Axiom: abbb=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] abbbbbb=abb

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

a aa aaa

Critical pair: abb=bba.

Reduce RHS:

[2]b(ba)
[2]⇒ (ba)bbb
⇒ abbbbbb

Flip LHS and RHS.

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

[4] bbbbbbbbb=bbb

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

b a aaa

Critical pair: bbb=abbbaa.

Reduce RHS:

[2]abb(ba)a
[2]⇒ ab(ba)bbba
[3]⇒ ab(abbbbbb)a
[2]⇒ a(ba)bba
[2]⇒ aabbbb(ba)
[2]⇒ aabbb(ba)bbb
[3]⇒ aabbb(abbbbbb)
[2]⇒ aabb(ba)bb
[2]⇒ aab(ba)bbbbb
[3]⇒ aab(abbbbbb)bb
[2]⇒ aa(ba)bbbb
[1]⇒ (aaa)bbbbbbb
⇒ bbbbbbbbb

Flip LHS and RHS.

Referenced by [6].

[5] bbbbbbbb=bbbb

Overlap of [1] aaa=bb with [3] abbbbbb=abb:

aa a abbbbbb

Critical pair: aaabb=bbbbbbbb.

Reduce LHS:

[1](aaa)bb
⇒ bbbb

Flip LHS and RHS.

Referenced by [6].

[6] bbbbb=bbb

Simplify [4] bbbbbbbbb=bbb.

Reduce LHS:

[5](bbbbbbbb)b
⇒ bbbbb

Defines rule #1.

Referenced by [7].

[7] abbbb=abb

Overlap of [3] abbbbbb=abb with [6] bbbbb=bbb:

a bbbbbb bbbbb

Critical pair: abbbb=abb.

Defines rule #2.