Certificate for #4869 ⟨a, b | abbabaab=aba⟩

Completion settings:

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

Axiom: abbabaab=aba.

Referenced by [4].

Axiom: ab=c.

Defines rule #3.

Referenced by [4], [5], [6], [7], [13], [14].

Axiom: ccaca=d.

Defines rule #17.

Referenced by [6], [10], [11], [15], [23], [29], [30], [31].

Simplify [1] abbabaab=aba.

Reduce RHS:

Referenced by [5].

Overlap of [4] abbabaab=ca with [2] ab=c:

Critical pair: cbabaab=ca.

Reduce LHS:

Defines rule #4.

Referenced by [7], [8], [11], [14], [16], [17], [20], [32].

Overlap of [3] ccaca=d with [2] ab=c:

Critical pair: ccacc=db.

Defines rule #6.

Referenced by [8], [9], [10], [12], [17], [18], [19], [21], [24], [28], [30], [32], [33].

Overlap of [5] cbcac=ca with [5] cbcac=ca:

Critical pair: cbcaca=cabcac.

Reduce LHS:

Reduce RHS:

Defines rule #16.

Referenced by [10], [11], [12], [13], [17], [20], [32].

Overlap of [6] ccacc=db with [5] cbcac=ca:

Critical pair: ccacca=dbbcac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [33].

Overlap of [6] ccacc=db with [6] ccacc=db:

Critical pair: ccacdb=dbcacc.

Flip LHS and RHS.

Referenced by [25].

Overlap of [3] ccaca=d with [7] caa=cccac:

Critical pair: ccacccac=da.

Reduce LHS:

Defines rule #13.

Referenced by [14], [17], [22], [25], [29], [30], [34].

Overlap of [5] cbcac=ca with [7] caa=cccac:

Critical pair: cbcacccac=caaa.

Reduce LHS:

Reduce RHS:

Defines rule #19.

Referenced by [15], [16], [17], [18], [19].

Overlap of [6] ccacc=db with [7] caa=cccac:

Critical pair: ccaccccac=dbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Referenced by [33].

Overlap of [7] caa=cccac with [2] ab=c:

Critical pair: cac=cccacb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [28].

Overlap of [10] dbcac=da with [5] cbcac=ca:

Critical pair: dbcaca=dabcac.

Reduce LHS:

Reduce RHS:

Referenced by [22], [26].

Overlap of [3] ccaca=d with [11] caccac=cd:

Critical pair: ccacd=dccac.

Flip LHS and RHS.

Referenced by [22], [26].

Overlap of [5] cbcac=ca with [11] caccac=cd:

Critical pair: cbcd=cacac.

Flip LHS and RHS.

Defines rule #18.

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

Overlap of [5] cbcac=ca with [11] caccac=cd:

Critical pair: cbcacd=caaccac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

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

Overlap of [6] ccacc=db with [11] caccac=cd:

Critical pair: ccd=dbac.

Flip LHS and RHS.

Defines rule #12.

Referenced by [28].

Overlap of [11] caccac=cd with [6] ccacc=db:

Critical pair: cadb=cdc.

Referenced by [23], [24], [35].

Overlap of [5] cbcac=ca with [17] cda=cad:

Critical pair: cbcacad=cada.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [6] ccacc=db with [17] cda=cad:

Critical pair: ccaccad=dbda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [27].

Overlap of [10] dbcac=da with [17] cda=cad:

Critical pair: dbcacad=dada.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Overlap of [3] ccaca=d with [19] cadb=cdc:

Critical pair: ccacdc=ddb.

Referenced by [34].

Overlap of [6] ccacc=db with [19] cadb=cdc:

Critical pair: ccaccdc=dbadb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [9] dbcacc=ccacdb with [10] dbcac=da:

Critical pair: dac=ccacdb.

Referenced by [29], [30], [37].

Simplify [14] daa=dccac.

Reduce RHS:

Defines rule #25.

Referenced by [27], [34].

Overlap of [21] dbda=dbad with [26] daa=ccacd:

Critical pair: dbccacd=dbada.

Flip LHS and RHS.

Defines rule #28.

Overlap of [6] ccacc=db with [13] cccacb=cac:

Critical pair: ccaccac=dbccacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [25] dac=ccacdb with [3] ccaca=d:

Critical pair: dad=ccacdbcaca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [25] dac=ccacdb with [6] ccacc=db:

Critical pair: dadb=ccacdbcacc.

Reduce RHS:

Referenced by [38].

Overlap of [3] ccaca=d with [16] cacac=cbcd:

Critical pair: ccbcd=dc.

Flip LHS and RHS.

Defines rule #2.

Referenced by [35], [36], [38].

Overlap of [5] cbcac=ca with [16] cacac=cbcd:

Critical pair: cbcbcd=caac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [37], [38].

Overlap of [8] dbbcac=dba with [16] cacac=cbcd:

Critical pair: dbbcbcd=dbaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [10] dbcac=da with [16] cacac=cbcd:

Critical pair: dbcbcd=daac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Simplify [19] cadb=cdc.

Reduce RHS:

Defines rule #9.

Simplify [24] dbadb=dbdc.

Reduce RHS:

Defines rule #21.

Simplify [25] dac=ccacdb.

Reduce RHS:

Defines rule #11.

Simplify [30] dadb=ddc.

Reduce RHS:

Defines rule #20.