Certificate for #3288 ⟨a, b | abbabababba=1⟩

Completion settings:

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

Axiom: abbabababba=1.

Referenced by [4].

Axiom: babb=c.

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

Axiom: aca=d.

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

Overlap of [1] abbabababba=1 with [2] babb=c:

Critical pair: abbabaca=1.

Reduce LHS:

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

Overlap of [2] babb=c with [4] abbabd=1:

Critical pair: b=cabd.

Flip LHS and RHS.

Referenced by [7].

Overlap of [3] aca=d with [4] abbabd=1:

Critical pair: ac=dbbabd.

Flip LHS and RHS.

Referenced by [10].

Overlap of [3] aca=d with [5] cabd=b:

Critical pair: ab=dbd.

Referenced by [8], [9], [10].

Overlap of [2] babb=c with [7] ab=dbd:

Critical pair: bdbdb=c.

Referenced by [9], [15], [20].

Overlap of [4] abbabd=1 with [7] ab=dbd:

Critical pair: dbdbabd=1.

Reduce LHS:

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

Overlap of [6] dbbabd=ac with [7] ab=dbd:

Critical pair: dbbdbdd=ac.

Flip LHS and RHS.

Referenced by [22].

Overlap of [9] dcdd=1 with [9] dcdd=1:

Critical pair: dcd=cdd.

Referenced by [12], [13], [16].

Overlap of [9] dcdd=1 with [11] dcd=cdd:

Critical pair: cddd=1.

Defines rule #2.

Referenced by [13], [14], [18], [19], [21], [23], [24], [25], [26], [27], [28].

Overlap of [11] dcd=cdd with [11] dcd=cdd:

Critical pair: dccdd=cddcd.

Reduce RHS:

Referenced by [14].

Overlap of [13] dccdd=c with [12] cddd=1:

Critical pair: dc=cd.

Defines rule #1.

Referenced by [15], [20], [21], [24], [25].

Overlap of [8] bdbdb=c with [8] bdbdb=c:

Critical pair: bdc=cdb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [11] dcd=cdd with [15] cdb=bcd:

Critical pair: dbcd=cddb.

Flip LHS and RHS.

Referenced by [17].

Overlap of [9] dcdd=1 with [16] cddb=dbcd:

Critical pair: ddbcd=b.

Referenced by [18].

Overlap of [17] ddbcd=b with [12] cddd=1:

Critical pair: ddb=bdd.

Referenced by [19], [20], [21], [22].

Overlap of [12] cddd=1 with [18] ddb=bdd:

Critical pair: cddbdd=db.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [20], [21], [22].

Overlap of [18] ddb=bdd with [8] bdbdb=c:

Critical pair: ddc=bdddbdb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [12] cddd=1 with [19] db=cbdddd:

Critical pair: cddcbdddd=b.

Reduce LHS:

Referenced by [24].

Simplify [10] ac=dbbdbdd.

Reduce RHS:

Referenced by [23].

Overlap of [22] ac=cbbcbdddddddddd with [12] cddd=1:

Critical pair: a=cbbcbddddddddddddd.

Defines rule #6.

Overlap of [21] ccbdddddd=b with [14] dc=cd:

Critical pair: ccbdddddcd=bc.

Reduce LHS:

Referenced by [25].

Overlap of [24] ccbddd=bc with [14] dc=cd:

Critical pair: ccbddcd=bcc.

Reduce LHS:

Defines rule #4.

Referenced by [26], [27].

Overlap of [25] ccb=bcc with [20] bcbcbdddddddddd=cdd:

Critical pair: cccdd=bcccbcbdddddddddd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [25] ccb=bcc with [26] bcbcbdddd=cccdd:

Critical pair: cccccdd=bcccbcbdddd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [27] bcbcbcd=cccccdd with [12] cddd=1:

Critical pair: bcbcb=cccccdddd.

Reduce RHS:

Defines rule #5.