Certificate for #3215 ⟨a, b | abaabbaabab=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. baab=c
  2. cac=d

Axiom: abaabbaabab=1.

Referenced by [4].

Axiom: baab=c.

Referenced by [4], [7], [8], [11].

Axiom: cac=d.

Referenced by [5], [6], [8], [9], [13], [16], [21], [24], [28].

Overlap of [1] abaabbaabab=1 with [2] baab=c:

Critical pair: acbaabab=1.

Reduce LHS:

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

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

Critical pair: cad=dac.

Flip LHS and RHS.

Referenced by [13], [27], [29].

Overlap of [3] cac=d with [4] accab=1:

Critical pair: c=dcab.

Flip LHS and RHS.

Referenced by [10], [12], [14], [21], [23].

Overlap of [2] baab=c with [2] baab=c:

Critical pair: baac=caab.

Referenced by [9].

Overlap of [4] accab=1 with [2] baab=c:

Critical pair: accac=aab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [9], [12].

Simplify [7] baac=caab.

Reduce RHS:

Referenced by [10].

Overlap of [9] baac=dd with [4] accab=1:

Critical pair: ba=ddcab.

Reduce RHS:

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

Overlap of [2] baab=c with [10] ba=dc:

Critical pair: baadc=ca.

Reduce LHS:

Referenced by [16], [17], [22], [24], [28].

Overlap of [10] ba=dc with [8] aab=acd:

Critical pair: bacd=dcab.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [13], [14], [15], [17], [21], [30].

Overlap of [12] dccd=c with [5] dac=cad:

Critical pair: dcccad=cac.

Reduce RHS:

Referenced by [19].

Overlap of [12] dccd=c with [6] dcab=c:

Critical pair: dccc=ccab.

Flip LHS and RHS.

Referenced by [18].

Overlap of [12] dccd=c with [12] dccd=c:

Critical pair: dccc=cccd.

Defines rule #1.

Referenced by [17], [18], [19], [20].

Overlap of [11] dcadc=ca with [11] dcadc=ca:

Critical pair: dcaca=caadc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [12] dccd=c with [11] dcadc=ca:

Critical pair: dccca=ccadc.

Reduce LHS:

Referenced by [19].

Overlap of [4] accab=1 with [14] ccab=dccc:

Critical pair: adccc=1.

Reduce LHS:

Defines rule #5.

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

Overlap of [13] dcccad=d with [15] dccc=cccd:

Critical pair: cccdad=d.

Reduce LHS:

Referenced by [23].

Overlap of [10] ba=dc with [18] acccd=1:

Critical pair: b=dccccd.

Reduce RHS:

Defines rule #3.

Referenced by [21].

Overlap of [18] acccd=1 with [6] dcab=c:

Critical pair: acccc=cab.

Reduce RHS:

Defines rule #4.

Referenced by [22], [26].

Overlap of [18] acccd=1 with [11] dcadc=ca:

Critical pair: acccca=cadc.

Reduce LHS:

Referenced by [26].

Overlap of [19] ccadcd=d with [6] dcab=c:

Critical pair: ccadcc=dcab.

Reduce RHS:

Referenced by [24], [25], [27].

Overlap of [11] dcadc=ca with [23] ccadcc=c:

Critical pair: dcadc=cacadcc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [26], [27], [28].

Overlap of [23] ccadcc=c with [23] ccadcc=c:

Critical pair: ccadc=cadcc.

Referenced by [28].

Overlap of [18] acccd=1 with [24] dadcc=ca:

Critical pair: acccca=adcc.

Reduce LHS:

Referenced by [28].

Overlap of [24] dadcc=ca with [23] ccadcc=c:

Critical pair: dadc=caadcc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [28], [30].

Overlap of [26] cadc=adcc with [11] dcadc=ca:

Critical pair: caca=adccadc.

Reduce LHS:

Reduce RHS:

Defines rule #7.

Referenced by [29], [30].

Overlap of [5] dac=cad with [28] da=ad:

Critical pair: adc=cad.

Flip LHS and RHS.

Referenced by [30].

Overlap of [12] dccd=c with [28] da=ad:

Critical pair: dccad=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.