Certificate for #4303 ⟨a, b | abababbba=ab⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(d) = deg(c) = 0, d < c; deg(a) = deg(e) = deg(b) = 1, a < e < b
• Auxiliary generators:
  1. ab=c
  2. cb=d
  3. dbdb=e

Axiom: abababbba=ab.

Referenced by [5].

Axiom: ab=c.

Defines rule #14.

Referenced by [5], [6], [7], [22], [24].

Axiom: cb=d.

Defines rule #3.

Referenced by [6], [7], [8], [23], [25].

Axiom: dbdb=e.

Defines rule #17.

Referenced by [12], [19], [21].

Simplify [1] abababbba=ab.

Reduce RHS:

Referenced by [6].

Overlap of [5] abababbba=c with [2] ab=c:

Critical pair: cababbba=c.

Reduce LHS:

Defines rule #13.

Referenced by [7], [9].

Overlap of [6] ccdba=c with [2] ab=c:

Critical pair: ccdbc=cb.

Reduce RHS:

Defines rule #9.

Referenced by [8], [9], [10], [11], [16], [20], [23], [25].

Overlap of [7] ccdbc=d with [3] cb=d:

Critical pair: ccdbd=db.

Defines rule #6.

Referenced by [10], [11], [12], [13], [14], [15], [16].

Overlap of [7] ccdbc=d with [6] ccdba=c:

Critical pair: ccdbc=dcdba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [13].

Overlap of [7] ccdbc=d with [7] ccdbc=d:

Critical pair: ccdbd=dcdbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [14], [15], [21].

Overlap of [7] ccdbc=d with [8] ccdbd=db:

Critical pair: ccdbdb=dcdbd.

Reduce LHS:

Referenced by [12], [14], [17].

Overlap of [8] ccdbd=db with [4] dbdb=e:

Critical pair: cce=dbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [14], [15], [16], [17].

Overlap of [8] ccdbd=db with [9] dcdba=d:

Critical pair: ccdbd=dbcdba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [20], [21].

Overlap of [8] ccdbd=db with [10] dcdbc=db:

Critical pair: ccdbdb=dbcdbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [10] dcdbc=db with [8] ccdbd=db:

Critical pair: dcdbdb=dbcdbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16], [18].

Overlap of [8] ccdbd=db with [12] dcdbd=cce:

Critical pair: ccdbcce=dbcdbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18].

Simplify [11] dbb=dcdbd.

Reduce RHS:

Defines rule #16.

Referenced by [19], [22], [24].

Simplify [15] dbcdbd=cceb.

Reduce RHS:

Defines rule #18.

Overlap of [4] dbdb=e with [17] dbb=cce:

Critical pair: dbcce=eb.

Flip LHS and RHS.

Defines rule #15.

Referenced by [23], [25].

Overlap of [7] ccdbc=d with [13] dbcdba=db:

Critical pair: ccdb=ddba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [24].

Overlap of [10] dcdbc=db with [13] dbcdba=db:

Critical pair: dcdb=dbdba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [22].

Overlap of [21] ea=dcdb with [2] ab=c:

Critical pair: ec=dcdbb.

Reduce RHS:

Defines rule #2.

Referenced by [23].

Overlap of [22] ec=dccce with [3] cb=d:

Critical pair: ed=dccceb.

Reduce RHS:

Defines rule #1.

Overlap of [20] ddba=ccdb with [2] ab=c:

Critical pair: ddbc=ccdbb.

Reduce RHS:

Defines rule #7.

Referenced by [25].

Overlap of [24] ddbc=cccce with [3] cb=d:

Critical pair: ddbd=cccceb.

Reduce RHS:

Defines rule #4.