Certificate for #16553 ⟨a, b | abb=aa, bbb=abb⟩

Back:⟨a, b | abb=aa, bbb=abb⟩

Completion settings:

[1] aa=abb

Axiom: abb=aa.

Flip LHS and RHS.

Referenced by [3].

[2] abb=bbb

Axiom: bbb=abb.

Flip LHS and RHS.

Defines rule #2.

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

[3] aa=bbb

Simplify [1] aa=abb.

Reduce RHS:

[2](abb)
⇒ bbb

Defines rule #4.

Referenced by [4], [5].

[4] bbba=bbbb

Overlap of [3] aa=bbb with [3] aa=bbb:

a a aa

Critical pair: abbb=bbba.

Reduce LHS:

[2](abb)b
⇒ bbbb

Flip LHS and RHS.

Defines rule #3.

[5] bbbbb=bbbb

Overlap of [3] aa=bbb with [2] abb=bbb:

a a abb

Critical pair: abbb=bbbbb.

Reduce LHS:

[2](abb)b
⇒ bbbb

Flip LHS and RHS.

Defines rule #1.