Certificate for #1523 ⟨a, b | ababbbabba=1⟩

Completion settings:

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

Axiom: ababbbabba=1.

Referenced by [4].

Axiom: bbabba=c.

Referenced by [4], [5].

Axiom: bab=d.

Defines rule #9.

Referenced by [4], [5], [6], [7], [10], [12], [22].

Overlap of [1] ababbbabba=1 with [3] bab=d:

Critical pair: adbbabba=1.

Reduce LHS:

Defines rule #1.

Referenced by [8], [9], [10], [14], [16], [19], [21], [24].

Overlap of [2] bbabba=c with [3] bab=d:

Critical pair: bdba=c.

Referenced by [7], [8], [13].

Overlap of [3] bab=d with [3] bab=d:

Critical pair: bad=dab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [10], [20].

Overlap of [5] bdba=c with [3] bab=d:

Critical pair: bdd=cb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [9].

Overlap of [5] bdba=c with [4] adc=1:

Critical pair: bdb=cdc.

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

Overlap of [4] adc=1 with [7] cb=bdd:

Critical pair: adbdd=b.

Referenced by [10], [11], [15].

Overlap of [9] adbdd=b with [6] dab=bad:

Critical pair: adbdbad=bab.

Reduce LHS:

Reduce RHS:

Referenced by [11].

Overlap of [9] adbdd=b with [10] dcad=d:

Critical pair: adbdd=bcad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [3] bab=d with [8] bdb=cdc:

Critical pair: bacdc=ddb.

Flip LHS and RHS.

Referenced by [23].

Overlap of [5] bdba=c with [8] bdb=cdc:

Critical pair: cdca=c.

Referenced by [14].

Overlap of [4] adc=1 with [13] cdca=c:

Critical pair: adc=dca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [15], [17], [24].

Overlap of [9] adbdd=b with [14] dca=1:

Critical pair: adbd=bca.

Referenced by [16], [17].

Overlap of [15] adbd=bca with [8] bdb=cdc:

Critical pair: adcdc=bcab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [15] adbd=bca with [14] dca=1:

Critical pair: adb=bcaca.

Referenced by [22].

Overlap of [16] bcab=dc with [11] bcad=b:

Critical pair: bcab=dccad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [4] adc=1 with [18] dccad=dc:

Critical pair: adc=cad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [20], [23].

Overlap of [19] cad=1 with [6] dab=bad:

Critical pair: cabad=ab.

Referenced by [21].

Overlap of [20] cabad=ab with [4] adc=1:

Critical pair: cab=abc.

Defines rule #7.

Referenced by [23].

Overlap of [17] adb=bcaca with [3] bab=d:

Critical pair: add=bcacaab.

Flip LHS and RHS.

Referenced by [24].

Overlap of [19] cad=1 with [12] ddb=bacdc:

Critical pair: cabacdc=db.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [22] bcacaab=add with [22] bcacaab=add:

Critical pair: bcacaaadd=addcacaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.