Certificate for #5821 ⟨a, b | abaaab=abbaa⟩

Completion settings:

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

Axiom: abaaab=abbaa.

Defines rule #6.

Referenced by [4], [5], [6], [7], [8], [12], [34], [41].

Axiom: aaba=c.

Defines rule #1.

Referenced by [3], [4], [5], [6], [8], [9], [10], [11], [12], [14], [15], [17], [18], [20], [26], [29], [35], [42], [53], [64], [81].

Overlap of [2] aaba=c with [2] aaba=c:

Critical pair: aabc=caba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [7], [21].

Overlap of [1] abaaab=abbaa with [2] aaba=c:

Critical pair: abac=abbaaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [8], [9], [10], [13], [22], [36], [43].

Overlap of [2] aaba=c with [1] abaaab=abbaa:

Critical pair: aabbaa=caab.

Defines rule #15.

Referenced by [12], [13], [14], [15], [16], [19], [23], [27], [29], [31], [54], [71].

Overlap of [2] aaba=c with [1] abaaab=abbaa:

Critical pair: aababbaa=cbaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

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

Overlap of [3] caba=aabc with [1] abaaab=abbaa:

Critical pair: cabbaa=aabcaab.

Defines rule #19.

Overlap of [1] abaaab=abbaa with [4] abbaaa=abac:

Critical pair: abaaabac=abbaabaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [15], [17], [18], [19], [24], [30], [38], [45], [52], [60], [67].

Overlap of [2] aaba=c with [4] abbaaa=abac:

Critical pair: aababac=cbbaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [11], [16], [25], [39], [46], [54], [65], [66], [69].

Overlap of [4] abbaaa=abac with [2] aaba=c:

Critical pair: abbac=abacba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [20], [21].

Overlap of [9] cbbaaa=cbac with [2] aaba=c:

Critical pair: cbbac=cbacba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [71], [72], [74], [76].

Overlap of [1] abaaab=abbaa with [5] aabbaa=caab:

Critical pair: abacaab=abbaabaa.

Reduce RHS:

Defines rule #8.

Referenced by [48], [49], [61].

Overlap of [4] abbaaa=abac with [5] aabbaa=caab:

Critical pair: abbacaab=abacbbaa.

Flip LHS and RHS.

Defines rule #28.

Overlap of [5] aabbaa=caab with [2] aaba=c:

Critical pair: aabbc=caabba.

Flip LHS and RHS.

Defines rule #23.

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

Overlap of [5] aabbaa=caab with [5] aabbaa=caab:

Critical pair: aabbcaab=caabbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #49.

Referenced by [52], [53], [54], [55], [56], [57], [58], [65].

Overlap of [9] cbbaaa=cbac with [5] aabbaa=caab:

Critical pair: cbbacaab=cbacbbaa.

Flip LHS and RHS.

Defines rule #40.

Overlap of [2] aaba=c with [8] abbcaa=abacc:

Critical pair: aababacc=cbbcaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [26], [27], [28], [33], [40], [47], [58], [62], [68].

Overlap of [8] abbcaa=abacc with [2] aaba=c:

Critical pair: abbcc=abaccba.

Flip LHS and RHS.

Defines rule #7.

Overlap of [8] abbcaa=abacc with [5] aabbaa=caab:

Critical pair: abbccaab=abaccbbaa.

Flip LHS and RHS.

Defines rule #32.

Overlap of [2] aaba=c with [10] abacba=abbac:

Critical pair: aabbac=ccba.

Defines rule #16.

Referenced by [22], [23], [24], [25], [28], [32], [55], [72].

Overlap of [3] caba=aabc with [10] abacba=abbac:

Critical pair: cabbac=aabccba.

Defines rule #20.

Overlap of [4] abbaaa=abac with [20] aabbac=ccba:

Critical pair: abbaccba=abacbbac.

Flip LHS and RHS.

Defines rule #29.

Overlap of [5] aabbaa=caab with [20] aabbac=ccba:

Critical pair: aabbccba=caabbbac.

Flip LHS and RHS.

Referenced by [59].

Overlap of [8] abbcaa=abacc with [20] aabbac=ccba:

Critical pair: abbcccba=abaccbbac.

Flip LHS and RHS.

Defines rule #33.

Overlap of [9] cbbaaa=cbac with [20] aabbac=ccba:

Critical pair: cbbaccba=cbacbbac.

Flip LHS and RHS.

Defines rule #41.

Overlap of [17] cbbcaa=cbacc with [2] aaba=c:

Critical pair: cbbcc=cbaccba.

Flip LHS and RHS.

Defines rule #13.

Referenced by [79].

Overlap of [17] cbbcaa=cbacc with [5] aabbaa=caab:

Critical pair: cbbccaab=cbaccbbaa.

Flip LHS and RHS.

Defines rule #44.

Overlap of [17] cbbcaa=cbacc with [20] aabbac=ccba:

Critical pair: cbbcccba=cbaccbbac.

Flip LHS and RHS.

Defines rule #45.

Overlap of [6] cbaaab=cbbaa with [5] aabbaa=caab:

Critical pair: cbacaab=cbbaabaa.

Reduce RHS:

Defines rule #14.

Referenced by [50], [51], [63], [80].

Overlap of [8] abbcaa=abacc with [14] caabba=aabbc:

Critical pair: abbaabbc=abaccbba.

Defines rule #57.

Overlap of [14] caabba=aabbc with [5] aabbaa=caab:

Critical pair: ccaab=aabbca.

Flip LHS and RHS.

Defines rule #17.

Referenced by [34], [35], [36], [37], [38], [39], [40], [48], [50], [56], [64], [73], [74], [82].

Overlap of [14] caabba=aabbc with [20] aabbac=ccba:

Critical pair: cccba=aabbcc.

Flip LHS and RHS.

Defines rule #18.

Referenced by [41], [42], [43], [44], [45], [46], [47], [49], [51], [57], [59], [64], [75], [76], [83].

Overlap of [17] cbbcaa=cbacc with [14] caabba=aabbc:

Critical pair: cbbaabbc=cbaccbba.

Defines rule #62.

Overlap of [1] abaaab=abbaa with [31] aabbca=ccaab:

Critical pair: abaccaab=abbaabca.

Flip LHS and RHS.

Defines rule #24.

Overlap of [2] aaba=c with [31] aabbca=ccaab:

Critical pair: aabccaab=cabbca.

Flip LHS and RHS.

Defines rule #21.

Overlap of [4] abbaaa=abac with [31] aabbca=ccaab:

Critical pair: abbaccaab=abacbbca.

Flip LHS and RHS.

Defines rule #30.

Overlap of [6] cbaaab=cbbaa with [31] aabbca=ccaab:

Critical pair: cbaccaab=cbbaabca.

Flip LHS and RHS.

Defines rule #36.

Overlap of [8] abbcaa=abacc with [31] aabbca=ccaab:

Critical pair: abbcccaab=abaccbbca.

Flip LHS and RHS.

Defines rule #34.

Overlap of [9] cbbaaa=cbac with [31] aabbca=ccaab:

Critical pair: cbbaccaab=cbacbbca.

Flip LHS and RHS.

Defines rule #42.

Overlap of [17] cbbcaa=cbacc with [31] aabbca=ccaab:

Critical pair: cbbcccaab=cbaccbbca.

Flip LHS and RHS.

Defines rule #46.

Overlap of [1] abaaab=abbaa with [32] aabbcc=cccba:

Critical pair: abacccba=abbaabcc.

Flip LHS and RHS.

Defines rule #25.

Overlap of [2] aaba=c with [32] aabbcc=cccba:

Critical pair: aabcccba=cabbcc.

Flip LHS and RHS.

Defines rule #22.

Overlap of [4] abbaaa=abac with [32] aabbcc=cccba:

Critical pair: abbacccba=abacbbcc.

Flip LHS and RHS.

Defines rule #31.

Overlap of [6] cbaaab=cbbaa with [32] aabbcc=cccba:

Critical pair: cbacccba=cbbaabcc.

Flip LHS and RHS.

Defines rule #37.

Overlap of [8] abbcaa=abacc with [32] aabbcc=cccba:

Critical pair: abbccccba=abaccbbcc.

Flip LHS and RHS.

Defines rule #35.

Overlap of [9] cbbaaa=cbac with [32] aabbcc=cccba:

Critical pair: cbbacccba=cbacbbcc.

Flip LHS and RHS.

Defines rule #43.

Overlap of [17] cbbcaa=cbacc with [32] aabbcc=cccba:

Critical pair: cbbccccba=cbaccbbcc.

Flip LHS and RHS.

Defines rule #47.

Overlap of [12] abacaab=abbca with [31] aabbca=ccaab:

Critical pair: abacccaab=abbcabca.

Flip LHS and RHS.

Defines rule #26.

Overlap of [12] abacaab=abbca with [32] aabbcc=cccba:

Critical pair: abaccccba=abbcabcc.

Flip LHS and RHS.

Defines rule #27.

Overlap of [29] cbacaab=cbbca with [31] aabbca=ccaab:

Critical pair: cbacccaab=cbbcabca.

Flip LHS and RHS.

Defines rule #38.

Overlap of [29] cbacaab=cbbca with [32] aabbcc=cccba:

Critical pair: cbaccccba=cbbcabcc.

Flip LHS and RHS.

Defines rule #39.

Overlap of [8] abbcaa=abacc with [15] caabbbaa=cccb:

Critical pair: abbcccb=abaccbbbaa.

Flip LHS and RHS.

Defines rule #60.

Overlap of [15] caabbbaa=cccb with [2] aaba=c:

Critical pair: caabbbc=cccbba.

Defines rule #48.

Referenced by [54], [55], [56], [57], [60], [61], [62], [63], [64], [65], [66], [69], [70], [77], [78], [84].

Overlap of [15] caabbbaa=cccb with [5] aabbaa=caab:

Critical pair: caabbbcaab=cccbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #51.

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

Overlap of [15] caabbbaa=cccb with [20] aabbac=ccba:

Critical pair: caabbbccba=cccbbbac.

Reduce LHS:

Defines rule #53.

Referenced by [78].

Overlap of [15] caabbbaa=cccb with [31] aabbca=ccaab:

Critical pair: caabbbccaab=cccbbbca.

Reduce LHS:

Defines rule #55.

Referenced by [81], [82], [83], [84].

Overlap of [15] caabbbaa=cccb with [32] aabbcc=cccba:

Critical pair: caabbbcccba=cccbbbcc.

Reduce LHS:

Defines rule #54.

Referenced by [69], [70], [77], [79], [80].

Overlap of [17] cbbcaa=cbacc with [15] caabbbaa=cccb:

Critical pair: cbbcccb=cbaccbbbaa.

Flip LHS and RHS.

Defines rule #65.

Simplify [23] caabbbac=aabbccba.

Reduce RHS:

Defines rule #50.

Referenced by [67], [68], [69].

Overlap of [8] abbcaa=abacc with [53] caabbbc=cccbba:

Critical pair: abbcccbba=abaccbbbc.

Flip LHS and RHS.

Defines rule #59.

Overlap of [12] abacaab=abbca with [53] caabbbc=cccbba:

Critical pair: abacccbba=abbcabbc.

Flip LHS and RHS.

Defines rule #58.

Overlap of [17] cbbcaa=cbacc with [53] caabbbc=cccbba:

Critical pair: cbbcccbba=cbaccbbbc.

Flip LHS and RHS.

Defines rule #64.

Overlap of [29] cbacaab=cbbca with [53] caabbbc=cccbba:

Critical pair: cbacccbba=cbbcabbc.

Flip LHS and RHS.

Defines rule #63.

Overlap of [31] aabbca=ccaab with [53] caabbbc=cccbba:

Critical pair: aabbcccbba=ccaababbbc.

Reduce LHS:

Reduce RHS:

Defines rule #56.

Referenced by [77].

Overlap of [53] caabbbc=cccbba with [15] caabbbaa=cccb:

Critical pair: caabbbcccb=cccbbaaabbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #78.

Overlap of [53] caabbbc=cccbba with [53] caabbbc=cccbba:

Critical pair: caabbbcccbba=cccbbaaabbbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #77.

Referenced by [73], [75].

Overlap of [8] abbcaa=abacc with [59] caabbbac=cccbaba:

Critical pair: abbcccbaba=abaccbbbac.

Flip LHS and RHS.

Defines rule #61.

Overlap of [17] cbbcaa=cbacc with [59] caabbbac=cccbaba:

Critical pair: cbbcccbaba=cbaccbbbac.

Flip LHS and RHS.

Defines rule #66.

Overlap of [53] caabbbc=cccbba with [59] caabbbac=cccbaba:

Critical pair: caabbbcccbaba=cccbbaaabbbac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #79.

Overlap of [53] caabbbc=cccbba with [54] cccbbbaa=cccbacb:

Critical pair: caabbbcccbacb=cccbbaccbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #82.

Overlap of [54] cccbbbaa=cccbacb with [5] aabbaa=caab:

Critical pair: cccbbbacaab=cccbacbabbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #69.

Overlap of [54] cccbbbaa=cccbacb with [20] aabbac=ccba:

Critical pair: cccbbbaccba=cccbacbabbac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #70.

Overlap of [54] cccbbbaa=cccbacb with [31] aabbca=ccaab:

Critical pair: cccbbbccaab=cccbacbbbca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #73.

Overlap of [54] cccbbbaa=cccbacb with [31] aabbca=ccaab:

Critical pair: cccbbbaccaab=cccbacbabbca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #71.

Overlap of [54] cccbbbaa=cccbacb with [32] aabbcc=cccba:

Critical pair: cccbbbcccba=cccbacbbbcc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #74.

Referenced by [78].

Overlap of [54] cccbbbaa=cccbacb with [32] aabbcc=cccba:

Critical pair: cccbbbacccba=cccbacbabbcc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #72.

Overlap of [53] caabbbc=cccbba with [64] cccbacbba=cccbbbc:

Critical pair: caabbbcccbbbc=cccbbaccbacbba.

Reduce LHS:

Reduce RHS:

Defines rule #81.

Overlap of [53] caabbbc=cccbba with [55] cccbbacba=cccbbbac:

Critical pair: caabbbcccbbbac=cccbbaccbbacba.

Reduce LHS:

Reduce RHS:

Defines rule #83.

Overlap of [57] cccbbaccba=cccbbbcc with [26] cbaccba=cbbcc:

Critical pair: cccbbaccbbcc=cccbbbccccba.

Defines rule #76.

Overlap of [57] cccbbaccba=cccbbbcc with [29] cbacaab=cbbca:

Critical pair: cccbbaccbbca=cccbbbcccaab.

Defines rule #75.

Overlap of [56] cccbbacaab=cccbbbca with [2] aaba=c:

Critical pair: cccbbacc=cccbbbcaa.

Flip LHS and RHS.

Defines rule #52.

Overlap of [56] cccbbacaab=cccbbbca with [31] aabbca=ccaab:

Critical pair: cccbbacccaab=cccbbbcabca.

Flip LHS and RHS.

Defines rule #67.

Overlap of [56] cccbbacaab=cccbbbca with [32] aabbcc=cccba:

Critical pair: cccbbaccccba=cccbbbcabcc.

Flip LHS and RHS.

Defines rule #68.

Overlap of [56] cccbbacaab=cccbbbca with [53] caabbbc=cccbba:

Critical pair: cccbbacccbba=cccbbbcabbc.

Flip LHS and RHS.

Defines rule #80.