Certificate for #4876 ⟨a, b | abbabbba=bab⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(a) = 0; deg(d) = deg(c) = 1, d < c; deg(b) = 2
• Auxiliary generators:
  1. ab=c
  2. cbb=d

Axiom: abbabbba=bab.

Referenced by [4].

Axiom: ab=c.

Defines rule #1.

Referenced by [4], [5], [6], [7], [8], [9], [10], [14], [15], [19], [22], [26], [31], [32], [34], [35].

Axiom: cbb=d.

Defines rule #15.

Referenced by [5], [7], [8], [11], [15], [21], [24].

Simplify [1] abbabbba=bab.

Reduce RHS:

Referenced by [5].

Overlap of [4] abbabbba=bc with [2] ab=c:

Critical pair: cbabbba=bc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [7], [8], [10], [12], [15], [17], [20], [26], [27], [34], [37], [40], [44].

Overlap of [2] ab=c with [5] bc=cbda:

Critical pair: acbda=cc.

Defines rule #2.

Referenced by [9].

Overlap of [3] cbb=d with [5] bc=cbda:

Critical pair: cbcbda=dc.

Reduce LHS:

Defines rule #11.

Referenced by [19].

Overlap of [5] bc=cbda with [3] cbb=d:

Critical pair: bd=cbdabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [10], [11], [12], [13], [16], [21], [25], [30].

Overlap of [6] acbda=cc with [2] ab=c:

Critical pair: acbdc=ccb.

Defines rule #5.

Referenced by [20], [33].

Overlap of [5] bc=cbda with [8] cbdcb=bd:

Critical pair: bbd=cbdabdcb.

Reduce RHS:

Defines rule #19.

Overlap of [8] cbdcb=bd with [3] cbb=d:

Critical pair: cbdd=bdb.

Flip LHS and RHS.

Defines rule #16.

Referenced by [13], [14], [15], [16], [17], [18], [23], [28], [36].

Overlap of [8] cbdcb=bd with [5] bc=cbda:

Critical pair: cbdccbda=bdc.

Defines rule #23.

Referenced by [34].

Overlap of [8] cbdcb=bd with [8] cbdcb=bd:

Critical pair: cbdbd=bddcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22], [23], [24], [25], [26], [29], [31], [32].

Overlap of [2] ab=c with [11] bdb=cbdd:

Critical pair: acbdd=cdb.

Defines rule #4.

Referenced by [26], [37].

Overlap of [3] cbb=d with [11] bdb=cbdd:

Critical pair: cbcbdd=ddb.

Reduce LHS:

Defines rule #13.

Overlap of [8] cbdcb=bd with [11] bdb=cbdd:

Critical pair: cbdccbdd=bddb.

Defines rule #26.

Overlap of [11] bdb=cbdd with [5] bc=cbda:

Critical pair: bdcbda=cbddc.

Referenced by [30], [31], [41].

Overlap of [11] bdb=cbdd with [11] bdb=cbdd:

Critical pair: bdcbdd=cbdddb.

Defines rule #25.

Referenced by [34], [40].

Overlap of [7] ccbdcda=dc with [2] ab=c:

Critical pair: ccbdcdc=dcb.

Defines rule #14.

Referenced by [20], [21], [33], [39].

Overlap of [5] bc=cbda with [19] ccbdcdc=dcb:

Critical pair: bdcb=cbdacbdcdc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [34].

Overlap of [19] ccbdcdc=dcb with [8] cbdcb=bd:

Critical pair: ccbdcdbd=dcbbdcb.

Reduce RHS:

Defines rule #21.

Overlap of [2] ab=c with [13] bddcb=ccbddd:

Critical pair: accbddd=cddcb.

Defines rule #6.

Referenced by [34].

Overlap of [11] bdb=cbdd with [13] bddcb=ccbddd:

Critical pair: bdccbddd=cbddddcb.

Defines rule #31.

Overlap of [13] bddcb=ccbddd with [3] cbb=d:

Critical pair: bddd=ccbdddb.

Flip LHS and RHS.

Defines rule #18.

Referenced by [27], [28], [29], [38], [43].

Overlap of [13] bddcb=ccbddd with [8] cbdcb=bd:

Critical pair: bddbd=ccbddddcb.

Defines rule #20.

Overlap of [14] acbdd=cdb with [13] bddcb=ccbddd:

Critical pair: acccbddd=cdbcb.

Reduce RHS:

Defines rule #7.

Overlap of [24] ccbdddb=bddd with [5] bc=cbda:

Critical pair: ccbdddcbda=bdddc.

Defines rule #24.

Overlap of [24] ccbdddb=bddd with [11] bdb=cbdd:

Critical pair: ccbdddcbdd=bddddb.

Defines rule #27.

Referenced by [44].

Overlap of [24] ccbdddb=bddd with [13] bddcb=ccbddd:

Critical pair: ccbdddccbddd=bdddddcb.

Defines rule #33.

Overlap of [8] cbdcb=bd with [17] bdcbda=cbddc:

Critical pair: ccbddc=bdda.

Referenced by [32], [33], [42].

Overlap of [17] bdcbda=cbddc with [2] ab=c:

Critical pair: bdcbdc=cbddcb.

Reduce RHS:

Defines rule #28.

Referenced by [43].

Overlap of [30] ccbddc=bdda with [13] bddcb=ccbddd:

Critical pair: ccccbddd=bddab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [33], [35], [36], [37], [38], [39], [40], [41], [42], [44].

Overlap of [30] ccbddc=bdda with [19] ccbdcdc=dcb:

Critical pair: ccbdddcb=bddacbdcdc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [12] cbdccbda=bdc with [22] accbddd=cddcb:

Critical pair: cbdccbdcddcb=bdcccbddd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #32.

Overlap of [2] ab=c with [32] bddc=ccccbddd:

Critical pair: accccbddd=cddc.

Defines rule #8.

Overlap of [11] bdb=cbdd with [32] bddc=ccccbddd:

Critical pair: bdccccbddd=cbddddc.

Defines rule #34.

Overlap of [14] acbdd=cdb with [32] bddc=ccccbddd:

Critical pair: acccccbddd=cdbc.

Reduce RHS:

Defines rule #9.

Overlap of [24] ccbdddb=bddd with [32] bddc=ccccbddd:

Critical pair: ccbdddccccbddd=bdddddc.

Defines rule #37.

Overlap of [32] bddc=ccccbddd with [19] ccbdcdc=dcb:

Critical pair: bdddcb=ccccbdddcbdcdc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #30.

Overlap of [18] bdcbdd=cbdddb with [32] bddc=ccccbddd:

Critical pair: bdcccccbddd=cbdddbc.

Reduce RHS:

Defines rule #36.

Simplify [17] bdcbda=cbddc.

Reduce RHS:

Defines rule #22.

Overlap of [30] ccbddc=bdda with [32] bddc=ccccbddd:

Critical pair: ccccccbddd=bdda.

Defines rule #10.

Overlap of [24] ccbdddb=bddd with [31] bdcbdc=cccbddd:

Critical pair: ccbdddcccbddd=bddddcbdc.

Defines rule #35.

Overlap of [28] ccbdddcbdd=bddddb with [32] bddc=ccccbddd:

Critical pair: ccbdddcccccbddd=bddddbc.

Reduce RHS:

Defines rule #38.