Certificate for #4734 ⟨a, b | aabbbbaa=abb⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1
• Auxiliary generators:
  1. abbb=c

Axiom: aabbbbaa=abb.

Referenced by [3].

Axiom: abbb=c.

Referenced by [3], [4].

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

Critical pair: acbaa=abb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [4], [5].

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

Critical pair: acbaab=c.

Defines rule #3.

Referenced by [5], [6].

Overlap of [4] acbaab=c with [3] abb=acbaa:

Critical pair: acbaacbaa=cb.

Defines rule #5.

Referenced by [6], [7].

Overlap of [5] acbaacbaa=cb with [4] acbaab=c:

Critical pair: acbac=cbb.

Flip LHS and RHS.

Defines rule #2.

Overlap of [5] acbaacbaa=cb with [5] acbaacbaa=cb:

Critical pair: acbacb=cbcbaa.

Flip LHS and RHS.

Defines rule #4.