Certificate for #1136 ⟨a, b | abbbba=abb⟩

Completion settings:

• Auxiliary generators:
  1. c = abbb
• Reduction order:
  • Left-to-right shortlex with c < b < a

Axiom: abbbba=abb.

Referenced by [3].

Axiom: abbb=c.

Referenced by [3], [4].

Overlap of [1] abbbba=abb with [2] abbb=c:

Critical pair: cba=abb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

Overlap of [2] abbb=c with [3] abb=cba:

Critical pair: cbab=c.

Defines rule #3.

Referenced by [5], [6].

Overlap of [4] cbab=c with [3] abb=cba:

Critical pair: cbcba=cb.

Defines rule #4.

Referenced by [6].

Overlap of [5] cbcba=cb with [4] cbab=c:

Critical pair: cbc=cbb.

Flip LHS and RHS.

Defines rule #1.