Certificate for #7054 ⟨a, b, c | ab=1, bcacc=c⟩

Completion settings:

• Auxiliary generators:
  1. d = ac
• Reduction order:
  • Left-to-right recursive path with deg(d) = deg(b) = 0, d < b; deg(c) = deg(a) = 1, c < a

Axiom: ab=1.

Defines rule #5.

Referenced by [5].

Axiom: bcacc=c.

Referenced by [4].

Axiom: ac=d.

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

Overlap of [2] bcacc=c with [3] ac=d:

Critical pair: bcdc=c.

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

Overlap of [1] ab=1 with [4] bcdc=c:

Critical pair: ac=cdc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [6], [7], [8], [10].

Overlap of [3] ac=d with [5] cdc=d:

Critical pair: ad=ddc.

Referenced by [9].

Overlap of [4] bcdc=c with [5] cdc=d:

Critical pair: bcdd=cdc.

Reduce RHS:

Referenced by [12].

Overlap of [5] cdc=d with [5] cdc=d:

Critical pair: cdd=ddc.

Flip LHS and RHS.

Referenced by [9], [13].

Simplify [6] ad=ddc.

Reduce RHS:

Referenced by [11].

Overlap of [4] bcdc=c with [5] cdc=d:

Critical pair: bd=c.

Flip LHS and RHS.

Defines rule #3.

Referenced by [11], [12], [13], [14].

Simplify [9] ad=cdd.

Reduce RHS:

Referenced by [16].

Overlap of [7] bcdd=d with [10] c=bd:

Critical pair: bbddd=d.

Referenced by [15].

Simplify [8] ddc=cdd.

Reduce RHS:

Referenced by [14].

Overlap of [13] ddc=bddd with [10] c=bd:

Critical pair: ddbd=bddd.

Flip LHS and RHS.

Defines rule #1.

Referenced by [15], [16].

Simplify [12] bbddd=d.

Reduce LHS:

Defines rule #2.

Simplify [11] ad=bddd.

Reduce RHS:

Defines rule #4.