Certificate for #5383 ⟨a, b | abbaaab=aaba⟩

Completion settings:

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

Axiom: abbaaab=aaba.

Referenced by [4].

Axiom: aab=c.

Defines rule #5.

Referenced by [4], [5], [6], [9], [15], [16].

Axiom: abbcb=d.

Defines rule #3.

Referenced by [6], [7], [11], [12], [78].

Simplify [1] abbaaab=aaba.

Reduce RHS:

Referenced by [5].

Overlap of [4] abbaaab=ca with [2] aab=c:

Critical pair: abbac=ca.

Defines rule #11.

Referenced by [9], [10], [11], [13], [22], [25], [28], [32], [53], [54], [79].

Overlap of [2] aab=c with [3] abbcb=d:

Critical pair: ad=cbcb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [7], [8], [10], [18], [64], [65], [66].

Overlap of [3] abbcb=d with [6] cbcb=ad:

Critical pair: abbad=dcb.

Defines rule #6.

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

Overlap of [6] cbcb=ad with [6] cbcb=ad:

Critical pair: cbad=adcb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [19], [20], [46], [47], [76], [77], [82], [84], [85], [87], [88].

Overlap of [2] aab=c with [5] abbac=ca:

Critical pair: aca=cbac.

Defines rule #10.

Referenced by [11], [12], [13], [14], [16], [17], [19], [21], [23], [27], [30], [35], [53], [64], [65], [66], [84].

Overlap of [5] abbac=ca with [6] cbcb=ad:

Critical pair: abbaad=cabcb.

Defines rule #12.

Referenced by [23], [24], [48], [57], [58], [61], [81].

Overlap of [5] abbac=ca with [9] aca=cbac:

Critical pair: abbcbac=caa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [15], [16], [17], [20], [37].

Overlap of [9] aca=cbac with [3] abbcb=d:

Critical pair: acd=cbacbbcb.

Flip LHS and RHS.

Defines rule #14.

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

Overlap of [9] aca=cbac with [5] abbac=ca:

Critical pair: acca=cbacbbac.

Flip LHS and RHS.

Defines rule #22.

Referenced by [28], [29], [30], [33], [76].

Overlap of [9] aca=cbac with [9] aca=cbac:

Critical pair: accbac=cbacca.

Defines rule #25.

Referenced by [31].

Overlap of [11] caa=dac with [2] aab=c:

Critical pair: cc=dacb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [18], [24], [26], [29], [34], [48], [55], [58], [59], [60], [62], [69], [70], [76], [77], [82], [84], [85], [87], [88].

Overlap of [11] caa=dac with [2] aab=c:

Critical pair: cac=dacab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

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

Overlap of [11] caa=dac with [9] aca=cbac:

Critical pair: cacbac=dacca.

Defines rule #21.

Referenced by [38].

Overlap of [15] dacb=cc with [6] cbcb=ad:

Critical pair: daad=cccb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [22], [39], [45], [47], [52], [55], [56], [67], [68], [71].

Overlap of [9] aca=cbac with [8] adcb=cbad:

Critical pair: accbad=cbacdcb.

Defines rule #17.

Referenced by [36].

Overlap of [11] caa=dac with [8] adcb=cbad:

Critical pair: cacbad=dacdcb.

Defines rule #15.

Referenced by [40].

Overlap of [9] aca=cbac with [7] abbad=dcb:

Critical pair: acdcb=cbacbbad.

Flip LHS and RHS.

Defines rule #16.

Referenced by [32], [33], [34], [35], [63], [77].

Overlap of [5] abbac=ca with [18] cccb=daad:

Critical pair: abbadaad=caccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [31], [36], [41], [46].

Overlap of [9] aca=cbac with [10] abbaad=cabcb:

Critical pair: accabcb=cbacbbaad.

Defines rule #24.

Referenced by [54], [55], [76], [77], [82], [85], [88].

Overlap of [10] abbaad=cabcb with [15] dacb=cc:

Critical pair: abbaacc=cabcbacb.

Defines rule #26.

Referenced by [28], [37], [38], [39], [40], [41], [42], [43], [44], [53], [54], [62], [83].

Overlap of [5] abbac=ca with [12] cbacbbcb=acd:

Critical pair: abbaacd=cabacbbcb.

Flip LHS and RHS.

Defines rule #23.

Referenced by [53], [84].

Overlap of [15] dacb=cc with [12] cbacbbcb=acd:

Critical pair: daacd=ccacbbcb.

Flip LHS and RHS.

Defines rule #18.

Referenced by [42], [49], [64], [72].

Overlap of [16] dcbacb=cac with [12] cbacbbcb=acd:

Critical pair: dcbaacd=cacacbbcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [56].

Overlap of [5] abbac=ca with [13] cbacbbac=acca:

Critical pair: abbaacca=cabacbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #33.

Referenced by [62], [63], [64], [65], [66], [85].

Overlap of [15] dacb=cc with [13] cbacbbac=acca:

Critical pair: daacca=ccacbbac.

Flip LHS and RHS.

Defines rule #32.

Referenced by [43], [50], [65], [73].

Overlap of [16] dcbacb=cac with [13] cbacbbac=acca:

Critical pair: dcbaacca=cacacbbac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #38.

Referenced by [67].

Overlap of [22] caccb=dcbaad with [14] accbac=cbacca:

Critical pair: ccbacca=dcbaadac.

Defines rule #30.

Referenced by [45], [46], [47], [48], [49], [50], [51], [55], [59].

Overlap of [5] abbac=ca with [21] cbacbbad=acdcb:

Critical pair: abbaacdcb=cabacbbad.

Defines rule #27.

Referenced by [41], [57], [59], [60], [61], [69], [86].

Overlap of [13] cbacbbac=acca with [21] cbacbbad=acdcb:

Critical pair: cbacbbaacdcb=accabacbbad.

Flip LHS and RHS.

Defines rule #45.

Referenced by [87], [88].

Overlap of [15] dacb=cc with [21] cbacbbad=acdcb:

Critical pair: daacdcb=ccacbbad.

Flip LHS and RHS.

Defines rule #20.

Referenced by [44], [51], [66], [74].

Overlap of [16] dcbacb=cac with [21] cbacbbad=acdcb:

Critical pair: dcbaacdcb=cacacbbad.

Reduce RHS:

Flip LHS and RHS.

Defines rule #31.

Referenced by [68].

Overlap of [22] caccb=dcbaad with [19] accbad=cbacdcb:

Critical pair: ccbacdcb=dcbaadad.

Defines rule #19.

Referenced by [52].

Overlap of [24] abbaacc=cabcbacb with [11] caa=dac:

Critical pair: abbaacdac=cabcbacbaa.

Flip LHS and RHS.

Defines rule #41.

Overlap of [24] abbaacc=cabcbacb with [17] cacbac=dacca:

Critical pair: abbaacdacca=cabcbacbacbac.

Flip LHS and RHS.

Defines rule #55.

Overlap of [24] abbaacc=cabcbacb with [18] cccb=daad:

Critical pair: abbaacdaad=cabcbacbccb.

Flip LHS and RHS.

Defines rule #39.

Overlap of [24] abbaacc=cabcbacb with [20] cacbad=dacdcb:

Critical pair: abbaacdacdcb=cabcbacbacbad.

Flip LHS and RHS.

Defines rule #49.

Overlap of [24] abbaacc=cabcbacb with [22] caccb=dcbaad:

Critical pair: abbaacdcbaad=cabcbacbaccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #48.

Referenced by [76], [77], [82], [84], [85], [87], [88].

Overlap of [24] abbaacc=cabcbacb with [26] ccacbbcb=daacd:

Critical pair: abbaacdaacd=cabcbacbcacbbcb.

Flip LHS and RHS.

Defines rule #53.

Overlap of [24] abbaacc=cabcbacb with [29] ccacbbac=daacca:

Critical pair: abbaacdaacca=cabcbacbcacbbac.

Flip LHS and RHS.

Defines rule #64.

Overlap of [24] abbaacc=cabcbacb with [34] ccacbbad=daacdcb:

Critical pair: abbaacdaacdcb=cabcbacbcacbbad.

Flip LHS and RHS.

Defines rule #54.

Overlap of [18] cccb=daad with [31] ccbacca=dcbaadac:

Critical pair: cdcbaadac=daadacca.

Flip LHS and RHS.

Defines rule #36.

Referenced by [57], [58], [60], [89].

Overlap of [22] caccb=dcbaad with [31] ccbacca=dcbaadac:

Critical pair: cadcbaadac=dcbaadacca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #43.

Referenced by [69].

Overlap of [31] ccbacca=dcbaadac with [8] adcb=cbad:

Critical pair: ccbacccbad=dcbaadacdcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #34.

Overlap of [31] ccbacca=dcbaadac with [10] abbaad=cabcb:

Critical pair: ccbacccabcb=dcbaadacbbaad.

Reduce RHS:

Defines rule #47.

Overlap of [31] ccbacca=dcbaadac with [26] ccacbbcb=daacd:

Critical pair: ccbadaacd=dcbaadaccbbcb.

Flip LHS and RHS.

Defines rule #42.

Overlap of [31] ccbacca=dcbaadac with [29] ccacbbac=daacca:

Critical pair: ccbadaacca=dcbaadaccbbac.

Flip LHS and RHS.

Defines rule #51.

Overlap of [31] ccbacca=dcbaadac with [34] ccacbbad=daacdcb:

Critical pair: ccbadaacdcb=dcbaadaccbbad.

Flip LHS and RHS.

Defines rule #44.

Overlap of [18] cccb=daad with [36] ccbacdcb=dcbaadad:

Critical pair: cdcbaadad=daadacdcb.

Flip LHS and RHS.

Defines rule #28.

Referenced by [61], [90].

Overlap of [24] abbaacc=cabcbacb with [25] cabacbbcb=abbaacd:

Critical pair: abbaacabbaacd=cabcbacbabacbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #56.

Overlap of [24] abbaacc=cabcbacb with [23] accabcb=cbacbbaad:

Critical pair: abbacbacbbaad=cabcbacbabcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #40.

Referenced by [62].

Overlap of [31] ccbacca=dcbaadac with [23] accabcb=cbacbbaad:

Critical pair: ccbacccbacbbaad=dcbaadacccabcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #62.

Overlap of [18] cccb=daad with [27] ccbaccbbcb=dcbaacd:

Critical pair: cdcbaacd=daadaccbbcb.

Flip LHS and RHS.

Defines rule #35.

Overlap of [10] abbaad=cabcb with [45] daadacca=cdcbaadac:

Critical pair: abbaacdcbaadac=cabcbaadacca.

Reduce LHS:

Defines rule #61.

Referenced by [70].

Overlap of [45] daadacca=cdcbaadac with [10] abbaad=cabcb:

Critical pair: daadacccabcb=cdcbaadacbbaad.

Reduce RHS:

Defines rule #52.

Overlap of [31] ccbacca=dcbaadac with [32] abbaacdcb=cabacbbad:

Critical pair: ccbacccabacbbad=dcbaadacbbaacdcb.

Reduce RHS:

Defines rule #63.

Overlap of [45] daadacca=cdcbaadac with [32] abbaacdcb=cabacbbad:

Critical pair: daadacccabacbbad=cdcbaadacbbaacdcb.

Reduce RHS:

Defines rule #67.

Overlap of [10] abbaad=cabcb with [52] daadacdcb=cdcbaadad:

Critical pair: abbaacdcbaadad=cabcbaadacdcb.

Reduce LHS:

Defines rule #50.

Overlap of [24] abbaacc=cabcbacb with [28] cabacbbac=cabcbacba:

Critical pair: abbaaccabcbacba=cabcbacbabacbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #65.

Overlap of [28] cabacbbac=cabcbacba with [21] cbacbbad=acdcb:

Critical pair: cabacbbaacdcb=cabcbacbabacbbad.

Flip LHS and RHS.

Defines rule #57.

Overlap of [28] cabacbbac=cabcbacba with [26] ccacbbcb=daacd:

Critical pair: cabacbbadaacd=cabcbacbacacbbcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #58.

Referenced by [76], [77].

Overlap of [28] cabacbbac=cabcbacba with [29] ccacbbac=daacca:

Critical pair: cabacbbadaacca=cabcbacbacacbbac.

Reduce RHS:

Referenced by [75].

Overlap of [28] cabacbbac=cabcbacba with [34] ccacbbad=daacdcb:

Critical pair: cabacbbadaacdcb=cabcbacbacacbbad.

Reduce RHS:

Defines rule #60.

Overlap of [18] cccb=daad with [30] ccbaccbbac=dcbaacca:

Critical pair: cdcbaacca=daadaccbbac.

Flip LHS and RHS.

Defines rule #46.

Overlap of [18] cccb=daad with [35] ccbaccbbad=dcbaacdcb:

Critical pair: cdcbaacdcb=daadaccbbad.

Flip LHS and RHS.

Defines rule #37.

Referenced by [91].

Overlap of [46] dcbaadacca=ccbadaadac with [32] abbaacdcb=cabacbbad:

Critical pair: dcbaadacccabacbbad=ccbadaadacbbaacdcb.

Reduce RHS:

Defines rule #72.

Overlap of [57] cabacbbadaadac=cabcbaadacca with [15] dacb=cc:

Critical pair: cabacbbadaacc=cabcbaadaccab.

Defines rule #59.

Referenced by [71], [72], [73], [74], [75], [76], [77], [92].

Overlap of [70] cabacbbadaacc=cabcbaadaccab with [18] cccb=daad:

Critical pair: cabacbbadaacdaad=cabcbaadaccabccb.

Flip LHS and RHS.

Defines rule #68.

Overlap of [70] cabacbbadaacc=cabcbaadaccab with [26] ccacbbcb=daacd:

Critical pair: cabacbbadaacdaacd=cabcbaadaccabcacbbcb.

Flip LHS and RHS.

Defines rule #79.

Overlap of [70] cabacbbadaacc=cabcbaadaccab with [29] ccacbbac=daacca:

Critical pair: cabacbbadaacdaacca=cabcbaadaccabcacbbac.

Flip LHS and RHS.

Defines rule #82.

Overlap of [70] cabacbbadaacc=cabcbaadaccab with [34] ccacbbad=daacdcb:

Critical pair: cabacbbadaacdaacdcb=cabcbaadaccabcacbbad.

Flip LHS and RHS.

Defines rule #80.

Overlap of [65] cabacbbadaacca=cabcbaadaccbbac with [70] cabacbbadaacc=cabcbaadaccab:

Critical pair: cabcbaadaccaba=cabcbaadaccbbac.

Defines rule #66.

Referenced by [78], [79], [80], [81], [82], [83], [84], [85], [86], [87], [88].

Overlap of [64] cabcbaadaccbbcb=cabacbbadaacd with [13] cbacbbac=acca:

Critical pair: cabcbaadaccbbacca=cabacbbadaacdacbbac.

Reduce RHS:

Defines rule #74.

Overlap of [64] cabcbaadaccbbcb=cabacbbadaacd with [21] cbacbbad=acdcb:

Critical pair: cabcbaadaccbbacdcb=cabacbbadaacdacbbad.

Reduce RHS:

Defines rule #69.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [3] abbcb=d:

Critical pair: cabcbaadaccabd=cabcbaadaccbbacbbcb.

Flip LHS and RHS.

Defines rule #70.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [5] abbac=ca:

Critical pair: cabcbaadaccabca=cabcbaadaccbbacbbac.

Flip LHS and RHS.

Defines rule #76.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [7] abbad=dcb:

Critical pair: cabcbaadaccabdcb=cabcbaadaccbbacbbad.

Flip LHS and RHS.

Defines rule #71.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [10] abbaad=cabcb:

Critical pair: cabcbaadaccabcabcb=cabcbaadaccbbacbbaad.

Flip LHS and RHS.

Defines rule #77.

Referenced by [89], [90], [91].

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [23] accabcb=cbacbbaad:

Critical pair: cabcbaadaccabcbacbbaad=cabcbaadaccbbacccabcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #81.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [24] abbaacc=cabcbacb:

Critical pair: cabcbaadaccabcabcbacb=cabcbaadaccbbacbbaacc.

Flip LHS and RHS.

Defines rule #83.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [25] cabacbbcb=abbaacd:

Critical pair: cabcbaadacabbaacd=cabcbaadaccbbaccbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #73.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [28] cabacbbac=cabcbacba:

Critical pair: cabcbaadaccabcbacba=cabcbaadaccbbaccbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #78.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [32] abbaacdcb=cabacbbad:

Critical pair: cabcbaadaccabcabacbbad=cabcbaadaccbbacbbaacdcb.

Defines rule #84.

Referenced by [92].

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [33] accabacbbad=cbacbbaacdcb:

Critical pair: cabcbaadcbacbbaacdcb=cabcbaadaccbbaccbbad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #75.

Overlap of [75] cabcbaadaccaba=cabcbaadaccbbac with [33] accabacbbad=cbacbbaacdcb:

Critical pair: cabcbaadaccabcbacbbaacdcb=cabcbaadaccbbacccabacbbad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #85.

Overlap of [81] cabcbaadaccbbacbbaad=cabcbaadaccabcabcb with [45] daadacca=cdcbaadac:

Critical pair: cabcbaadaccbbacbbaacdcbaadac=cabcbaadaccabcabcbaadacca.

Defines rule #89.

Overlap of [81] cabcbaadaccbbacbbaad=cabcbaadaccabcabcb with [52] daadacdcb=cdcbaadad:

Critical pair: cabcbaadaccbbacbbaacdcbaadad=cabcbaadaccabcabcbaadacdcb.

Defines rule #86.

Overlap of [81] cabcbaadaccbbacbbaad=cabcbaadaccabcabcb with [68] daadaccbbad=cdcbaacdcb:

Critical pair: cabcbaadaccbbacbbaacdcbaacdcb=cabcbaadaccabcabcbaadaccbbad.

Defines rule #88.

Overlap of [86] cabcbaadaccabcabacbbad=cabcbaadaccbbacbbaacdcb with [70] cabacbbadaacc=cabcbaadaccab:

Critical pair: cabcbaadaccabcabcbaadaccab=cabcbaadaccbbacbbaacdcbaacc.

Flip LHS and RHS.

Defines rule #87.