Certificate for #16459 ⟨a, b | aba=bb, abbb=aa⟩

Back:⟨a, b | aba=bb, abbb=aa⟩

Completion settings:

[1] aba=bb

Axiom: aba=bb.

Defines rule #5.

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

[2] aa=abbb

Axiom: abbb=aa.

Flip LHS and RHS.

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

[3] bbba=abbb

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

ab a aba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Referenced by [5].

[4] bba=bbbbb

Overlap of [1] aba=bb with [2] aa=abbb:

ab a aa

Critical pair: ababbb=bba.

Reduce LHS:

[1](aba)bbb
⇒ bbbbb

Flip LHS and RHS.

Defines rule #3.

[5] abb=bbbbb

Overlap of [2] aa=abbb with [1] aba=bb:

a a aba

Critical pair: abb=abbbba.

Reduce RHS:

[3]ab(bbba)
[1]⇒ (aba)bbb
⇒ bbbbb

Defines rule #2.

Referenced by [6], [7].

[6] bbbbbbbbb=bbbb

Overlap of [1] aba=bb with [5] abb=bbbbb:

ab a abb

Critical pair: abbbbbb=bbbb.

Reduce LHS:

[5](abb)bbbb
⇒ bbbbbbbbb

Defines rule #1.

[7] aa=bbbbbb

Simplify [2] aa=abbb.

Reduce RHS:

[5](abb)b
⇒ bbbbbb

Defines rule #4.