Certificate for #17137 ⟨a, b | aaaa=1, abbbba=b⟩

Completion settings:

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

Axiom: aaaa=1.

Defines rule #20.

Referenced by [6], [8], [11], [12], [27], [39].

Axiom: abbbba=b.

Referenced by [5].

Axiom: bbba=c.

Referenced by [5], [7], [9], [14], [16], [17], [18], [19], [23], [25].

Axiom: accc=d.

Referenced by [8], [9], [15], [20], [21], [28].

Overlap of [2] abbbba=b with [3] bbba=c:

Critical pair: abc=b.

Referenced by [6], [7], [10], [13], [16], [20].

Overlap of [1] aaaa=1 with [5] abc=b:

Critical pair: aaab=bc.

Referenced by [10], [12].

Overlap of [3] bbba=c with [5] abc=b:

Critical pair: bbbb=cbc.

Flip LHS and RHS.

Defines rule #13.

Referenced by [13], [17], [18], [21], [22], [53].

Overlap of [1] aaaa=1 with [4] accc=d:

Critical pair: aaad=ccc.

Referenced by [14], [27].

Overlap of [3] bbba=c with [4] accc=d:

Critical pair: bbbd=cccc.

Flip LHS and RHS.

Referenced by [11], [27], [28], [40], [43].

Overlap of [6] aaab=bc with [5] abc=b:

Critical pair: aab=bcc.

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

Overlap of [1] aaaa=1 with [10] aab=bcc:

Critical pair: aabcc=b.

Reduce LHS:

Defines rule #2.

Referenced by [21], [41], [51], [52], [53].

Overlap of [1] aaaa=1 with [10] aab=bcc:

Critical pair: aaabcc=ab.

Reduce LHS:

Referenced by [14], [26].

Overlap of [5] abc=b with [7] cbc=bbbb:

Critical pair: abbbbb=bbc.

Referenced by [30].

Overlap of [3] bbba=c with [8] aaad=ccc:

Critical pair: bbbccc=caad.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [4] accc=d with [14] caad=bbab:

Critical pair: accbbab=daad.

Referenced by [33].

Overlap of [5] abc=b with [14] caad=bbab:

Critical pair: abbbab=baad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19], [24].

Overlap of [7] cbc=bbbb with [14] caad=bbab:

Critical pair: cbbbab=bbbbaad.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [7] cbc=bbbb with [17] bcad=ccb:

Critical pair: cccb=bbbbad.

Reduce RHS:

Referenced by [20], [21], [22], [34], [40], [44].

Overlap of [3] bbba=c with [16] baad=acb:

Critical pair: bbacb=cad.

Referenced by [35].

Overlap of [4] accc=d with [18] cccb=bcd:

Critical pair: abcd=db.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [23], [24], [28], [34], [39], [40], [42], [44], [47], [48], [49], [50], [51], [52], [54], [55].

Overlap of [4] accc=d with [18] cccb=bcd:

Critical pair: acbcd=dcb.

Reduce LHS:

Defines rule #9.

Referenced by [25], [26], [29], [30], [31], [34], [39].

Overlap of [18] cccb=bcd with [7] cbc=bbbb:

Critical pair: ccbbbb=bcdc.

Flip LHS and RHS.

Defines rule #14.

Overlap of [20] db=bd with [3] bbba=c:

Critical pair: dc=bdbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [41], [42], [46].

Overlap of [20] db=bd with [16] baad=acb:

Critical pair: dacb=bdaad.

Flip LHS and RHS.

Referenced by [37].

Overlap of [21] ab=dcb with [3] bbba=c:

Critical pair: ac=dcbbba.

Reduce RHS:

Defines rule #18.

Referenced by [27], [28], [34], [36], [37].

Overlap of [21] ab=dcb with [12] bccc=ab:

Critical pair: aab=dcbccc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [45].

Overlap of [1] aaaa=1 with [25] ac=dcc:

Critical pair: aaadcc=c.

Reduce LHS:

Referenced by [40], [43].

Overlap of [4] accc=d with [25] ac=dcc:

Critical pair: dcccc=d.

Reduce LHS:

Defines rule #3.

Referenced by [29], [42], [54].

Overlap of [21] ab=dcb with [28] bbbdd=d:

Critical pair: ad=dcbbbdd.

Reduce RHS:

Defines rule #10.

Referenced by [32], [33], [35], [38], [39].

Overlap of [13] abbbbb=bbc with [21] ab=dcb:

Critical pair: dcbbbbb=bbc.

Flip LHS and RHS.

Defines rule #5.

Referenced by [50].

Simplify [14] caad=bbab.

Reduce RHS:

Referenced by [32].

Overlap of [31] caad=bbdcb with [29] ad=dcd:

Critical pair: cadcd=bbdcb.

Reduce LHS:

Referenced by [39].

Simplify [15] accbbab=daad.

Reduce RHS:

Referenced by [34].

Overlap of [33] accbbab=ddcdcd with [25] ac=dcc:

Critical pair: dcccbbab=ddcdcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [38], [48].

Simplify [19] bbacb=cad.

Reduce RHS:

Referenced by [36].

Overlap of [35] bbacb=cdcd with [25] ac=dcc:

Critical pair: bbdccb=cdcd.

Referenced by [49].

Simplify [24] bdaad=dacb.

Reduce RHS:

Referenced by [38].

Overlap of [37] bdaad=ddccb with [29] ad=dcd:

Critical pair: bdadcd=ddccb.

Reduce LHS:

Referenced by [49].

Overlap of [1] aaaa=1 with [29] ad=dcd:

Critical pair: aaadcd=d.

Reduce LHS:

Referenced by [47].

Overlap of [18] cccb=bcd with [27] bbbdc=c:

Critical pair: cccc=bcdbbdc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [11] bbbbd=b with [23] bbbda=dc:

Critical pair: bdc=ba.

Flip LHS and RHS.

Defines rule #11.

Overlap of [20] db=bd with [23] bbbda=dc:

Critical pair: ddc=bdbbda.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [9] cccc=bbbd with [9] cccc=bbbd:

Critical pair: cbbbd=bbbdc.

Reduce RHS:

Defines rule #4.

Referenced by [44], [45], [46], [47], [51], [52], [55].

Overlap of [18] cccb=bcd with [43] cbbbd=c:

Critical pair: ccc=bcdbbd.

Reduce RHS:

Defines rule #19.

Overlap of [26] dcdcb=bcc with [43] cbbbd=c:

Critical pair: dcdc=bccbbd.

Defines rule #15.

Referenced by [48].

Overlap of [43] cbbbd=c with [23] bbbda=dc:

Critical pair: cdc=ca.

Flip LHS and RHS.

Defines rule #17.

Overlap of [39] dcbbddcb=d with [43] cbbbd=c:

Critical pair: dcbbddc=dbbd.

Reduce RHS:

Referenced by [51], [52], [54].

Overlap of [34] ddcdcd=bdcbddcb with [45] dcdc=bccbbd:

Critical pair: dbccbbdd=bdcbddcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [49].

Overlap of [38] bbdcbddcb=ddccb with [48] bdcbddcb=bdccbbdd:

Critical pair: bbdccbbdd=ddccb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [55].

Overlap of [20] db=bd with [30] bbc=dcbbbbb:

Critical pair: ddcbbbbb=bdbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [40] bcbbddc=bbbd with [47] dcbbddc=bbdd:

Critical pair: bcbbdbbdd=bbbdbbddc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [52].

Overlap of [51] bbddc=bcbdd with [47] dcbbddc=bbdd:

Critical pair: bbdbbdd=bcbddbbddc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [53], [54].

Overlap of [7] cbc=bbbb with [52] bcdddc=bdd:

Critical pair: cbdd=bbbbdddc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Overlap of [52] bcdddc=bdd with [47] dcbbddc=bbdd:

Critical pair: bcddbbdd=bddbbddc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [49] ddccb=cdcbddd with [43] cbbbd=c:

Critical pair: ddcc=cdcbdddbbd.

Reduce RHS:

Defines rule #16.