Certificate for #1519 ⟨a, b | ababbaabba=1⟩

Completion settings:

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

Axiom: ababbaabba=1.

Referenced by [4].

Axiom: ba=c.

Defines rule #5.

Referenced by [4], [5], [8], [11], [13], [16], [22], [25], [39], [40].

Axiom: bcca=d.

Referenced by [6], [7], [17], [18], [25], [26], [36].

Overlap of [1] ababbaabba=1 with [2] ba=c:

Critical pair: acbbaabba=1.

Reduce LHS:

Referenced by [5], [6], [7], [9], [11], [12], [15], [26], [28], [32].

Overlap of [2] ba=c with [4] acbcabc=1:

Critical pair: b=ccbcabc.

Flip LHS and RHS.

Referenced by [9], [10], [13], [16], [27], [29].

Overlap of [3] bcca=d with [4] acbcabc=1:

Critical pair: bcc=dcbcabc.

Flip LHS and RHS.

Referenced by [10], [13], [17], [30].

Overlap of [4] acbcabc=1 with [3] bcca=d:

Critical pair: acbcad=ca.

Referenced by [8], [14].

Overlap of [2] ba=c with [7] acbcad=ca:

Critical pair: bca=ccbcad.

Flip LHS and RHS.

Referenced by [21].

Overlap of [4] acbcabc=1 with [5] ccbcabc=b:

Critical pair: acbcabb=cbcabc.

Referenced by [11], [18], [31].

Overlap of [6] dcbcabc=bcc with [5] ccbcabc=b:

Critical pair: dcbcabb=bcccbcabc.

Reduce RHS:

Referenced by [19].

Overlap of [9] acbcabb=cbcabc with [2] ba=c:

Critical pair: acbcabc=cbcabca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12], [13], [14], [19], [20], [23].

Overlap of [4] acbcabc=1 with [11] cbcabca=1:

Critical pair: acbcab=bcabca.

Referenced by [14].

Overlap of [6] dcbcabc=bcc with [11] cbcabca=1:

Critical pair: dcbcab=bccbcabca.

Reduce RHS:

Referenced by [14].

Overlap of [7] acbcad=ca with [13] dcbcab=bc:

Critical pair: acbcabc=cacbcab.

Reduce LHS:

Reduce RHS:

Referenced by [15], [16], [17], [18], [19], [20], [21], [24].

Overlap of [4] acbcabc=1 with [14] bcabcac=1:

Critical pair: acbca=abcac.

Referenced by [18], [26], [28], [31], [32].

Overlap of [5] ccbcabc=b with [14] bcabcac=1:

Critical pair: ccbca=babcac.

Reduce RHS:

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

Overlap of [6] dcbcabc=bcc with [14] bcabcac=1:

Critical pair: dcbca=bccabcac.

Reduce RHS:

Referenced by [19], [30].

Overlap of [9] acbcabb=cbcabc with [14] bcabcac=1:

Critical pair: acbcab=cbcabccabcac.

Reduce LHS:

Reduce RHS:

Referenced by [26], [28], [31], [32], [33].

Overlap of [10] dcbcabb=bcb with [14] bcabcac=1:

Critical pair: dcbcab=bcbcabcac.

Reduce LHS:

Reduce RHS:

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

Overlap of [11] cbcabca=1 with [14] bcabcac=1:

Critical pair: cbca=bcac.

Defines rule #6.

Referenced by [21], [23], [25], [26], [27], [28], [29], [31], [32], [33], [37].

Overlap of [8] ccbcad=bca with [19] dbcacb=bc:

Critical pair: ccbcabc=bcabcacb.

Reduce LHS:

Reduce RHS:

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

Overlap of [19] dbcacb=bc with [2] ba=c:

Critical pair: dbcacc=bca.

Referenced by [26].

Overlap of [11] cbcabca=1 with [21] bcaccbc=b:

Critical pair: cbcab=ccbc.

Reduce LHS:

Referenced by [25], [26], [31], [34].

Overlap of [14] bcabcac=1 with [21] bcaccbc=b:

Critical pair: bcab=cbc.

Referenced by [50].

Overlap of [21] bcaccbc=b with [20] cbca=bcac:

Critical pair: bcacbcac=ba.

Reduce LHS:

Reduce RHS:

Referenced by [26], [27].

Overlap of [4] acbcabc=1 with [25] ccdc=c:

Critical pair: acbcabc=cdc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27], [32], [35].

Overlap of [5] ccbcabc=b with [25] ccdc=c:

Critical pair: ccbcabc=bcdc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [28], [29], [30], [31].

Overlap of [4] acbcabc=1 with [27] bccd=b:

Critical pair: acbcab=cd.

Reduce LHS:

Referenced by [31], [32], [33], [36].

Overlap of [5] ccbcabc=b with [27] bccd=b:

Critical pair: ccbcab=bcd.

Reduce LHS:

Referenced by [36].

Overlap of [6] dcbcabc=bcc with [27] bccd=b:

Critical pair: dcbcab=bcccd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [9] acbcabb=cbcabc with [27] bccd=b:

Critical pair: acbcabb=cbcabcccd.

Reduce LHS:

Reduce RHS:

Referenced by [36].

Overlap of [4] acbcabc=1 with [15] acbca=abcac:

Critical pair: abcacbc=1.

Reduce LHS:

Defines rule #2.

Referenced by [35], [38], [41], [42], [44], [45], [47], [48], [51], [52].

Simplify [18] abcacb=cbcadbcac.

Reduce RHS:

Referenced by [34].

Overlap of [33] abcacb=cd with [23] bcacb=ccbc:

Critical pair: accbc=cd.

Referenced by [37], [38], [42].

Simplify [26] cdc=ccd.

Reduce RHS:

Referenced by [36].

Overlap of [28] bcacdbcac=cd with [31] cdb=ccbccccd:

Critical pair: bcaccbccccdcac=cd.

Reduce LHS:

Defines rule #1.

Referenced by [38], [42], [43], [45], [47], [51], [52].

Overlap of [34] accbc=cd with [20] cbca=bcac:

Critical pair: acbcac=cda.

Reduce LHS:

Referenced by [46].

Overlap of [34] accbc=cd with [32] ccd=1:

Critical pair: accb=cdcd.

Reduce RHS:

Defines rule #10.

Referenced by [39], [40], [42], [49].

Overlap of [2] ba=c with [38] accb=d:

Critical pair: bd=cccb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [42], [49].

Overlap of [38] accb=d with [2] ba=c:

Critical pair: accc=da.

Flip LHS and RHS.

Defines rule #3.

Referenced by [41], [46].

Overlap of [32] ccd=1 with [40] da=accc:

Critical pair: ccaccc=a.

Referenced by [44].

Overlap of [34] accbc=cd with [39] cccb=bd:

Critical pair: accbbd=cdccb.

Reduce LHS:

Reduce RHS:

Referenced by [43].

Overlap of [42] dbd=cb with [36] dc=cd:

Critical pair: dbcd=cbc.

Referenced by [47].

Overlap of [41] ccaccc=a with [32] ccd=1:

Critical pair: ccac=ad.

Referenced by [45].

Overlap of [44] ccac=ad with [32] ccd=1:

Critical pair: cca=adcd.

Reduce RHS:

Defines rule #4.

Referenced by [51], [52].

Simplify [37] abcacc=cda.

Reduce RHS:

Referenced by [48], [49].

Overlap of [43] dbcd=cbc with [36] dc=cd:

Critical pair: dbccd=cbcc.

Reduce LHS:

Defines rule #7.

Referenced by [51], [52].

Overlap of [46] abcacc=caccc with [32] ccd=1:

Critical pair: abca=cacccd.

Reduce RHS:

Defines rule #9.

Referenced by [50].

Overlap of [46] abcacc=caccc with [38] accb=d:

Critical pair: abcd=cacccb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [48] abca=cac with [24] bcab=cbc:

Critical pair: acbc=cacb.

Flip LHS and RHS.

Defines rule #12.

Overlap of [45] cca=acdd with [49] cabd=abcd:

Critical pair: cabcd=acddbd.

Reduce RHS:

Referenced by [52].

Overlap of [45] cca=acdd with [51] cabcd=ab:

Critical pair: cab=acddbcd.

Reduce RHS:

Defines rule #11.