Certificate for #7791 ⟨a, b | aaa=1, ababb=ba⟩

Completion settings:

• Auxiliary generators:
  1. c = baab
• Reduction order:
  • Right-to-left shortlex with a < c < b

Axiom: aaa=1.

Defines rule #1.

Referenced by [5], [6], [8], [12], [13], [15], [18], [19], [20], [23], [25], [26], [28], [30], [31], [34], [39], [43], [45], [48], [49], [50], [51], [53], [55], [56], [57], [58], [60], [61], [63], [66], [67], [69], [70], [71], [72], [73], [74], [76], [78], [81], [82], [83], [84], [85], [87].

Axiom: ababb=ba.

Referenced by [5], [6], [7].

Axiom: baab=c.

Defines rule #11.

Referenced by [4], [6], [7], [9], [10], [11], [21], [24], [32], [40], [48], [55], [59], [62], [64], [65], [68].

Overlap of [3] baab=c with [3] baab=c:

Critical pair: baac=caab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [14], [18], [19], [20], [22], [25], [27], [31], [34], [46], [49], [51], [53], [56], [57], [62], [67], [83].

Overlap of [1] aaa=1 with [2] ababb=ba:

Critical pair: aaba=babb.

Flip LHS and RHS.

Defines rule #17.

Referenced by [9], [30], [43], [55], [61], [62], [63], [65], [66], [69], [70], [72], [86].

Overlap of [2] ababb=ba with [3] baab=c:

Critical pair: ababc=baaab.

Reduce RHS:

Defines rule #18.

Referenced by [8], [9], [10], [14], [17], [30], [33], [44], [47], [61], [76], [78], [79], [86].

Overlap of [3] baab=c with [2] ababb=ba:

Critical pair: baba=cabb.

Flip LHS and RHS.

Defines rule #16.

Referenced by [62], [63], [65], [66], [67], [69], [70], [71], [72], [84], [87].

Overlap of [1] aaa=1 with [6] ababc=bb:

Critical pair: aabb=babc.

Defines rule #15.

Referenced by [21], [22].

Overlap of [3] baab=c with [6] ababc=bb:

Critical pair: babb=cabc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [10], [11], [15], [28], [32], [55], [59], [76], [78].

Overlap of [6] ababc=bb with [9] cabc=aaba:

Critical pair: ababaaba=bbabc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21], [39].

Overlap of [9] cabc=aaba with [9] cabc=aaba:

Critical pair: cabaaba=aabaabc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [12], [71], [75].

Overlap of [1] aaa=1 with [11] aacc=caca:

Critical pair: acaca=cc.

Referenced by [13], [14], [15], [16].

Overlap of [12] acaca=cc with [1] aaa=1:

Critical pair: acac=ccaa.

Defines rule #2.

Referenced by [14], [18], [25], [48].

Overlap of [12] acaca=cc with [6] ababc=bb:

Critical pair: acacbb=ccbabc.

Reduce LHS:

Referenced by [29], [35].

Overlap of [12] acaca=cc with [9] cabc=aaba:

Critical pair: acaaaba=ccbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [17], [19], [35], [62].

Overlap of [12] acaca=cc with [12] acaca=cc:

Critical pair: accc=ccca.

Defines rule #5.

Referenced by [20], [36], [63].

Overlap of [6] ababc=bb with [15] ccbc=acba:

Critical pair: ababacba=bbcbc.

Referenced by [40].

Overlap of [13] acac=ccaa with [4] caab=baac:

Critical pair: acabaac=ccaaaab.

Reduce RHS:

Defines rule #37.

Overlap of [15] ccbc=acba with [4] caab=baac:

Critical pair: ccbbaac=acbaaab.

Reduce RHS:

Defines rule #41.

Overlap of [16] accc=ccca with [4] caab=baac:

Critical pair: accbaac=cccaaab.

Reduce RHS:

Defines rule #39.

Overlap of [3] baab=c with [8] aabb=babc:

Critical pair: bbabc=cb.

Reduce LHS:

Referenced by [23], [24], [25], [26], [27], [28], [29].

Overlap of [4] caab=baac with [8] aabb=babc:

Critical pair: cbabc=baacb.

Flip LHS and RHS.

Referenced by [37], [41].

Overlap of [1] aaa=1 with [21] abaca=cb:

Critical pair: aacb=baca.

Defines rule #12.

Referenced by [36], [38], [41], [48], [52], [54], [67].

Overlap of [3] baab=c with [21] abaca=cb:

Critical pair: bacb=caca.

Defines rule #14.

Overlap of [4] caab=baac with [21] abaca=cb:

Critical pair: cacb=baacaca.

Reduce RHS:

Defines rule #13.

Referenced by [35], [36], [37], [38], [50], [52], [54], [58].

Overlap of [21] abaca=cb with [1] aaa=1:

Critical pair: abac=cbaa.

Defines rule #3.

Referenced by [29], [39], [40], [64].

Overlap of [21] abaca=cb with [4] caab=baac:

Critical pair: ababaac=cbab.

Defines rule #38.

Referenced by [73], [74].

Overlap of [21] abaca=cb with [9] cabc=aaba:

Critical pair: abaaaba=cbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [30], [31], [32], [37], [43], [55], [65].

Overlap of [21] abaca=cb with [21] abaca=cb:

Critical pair: abaccb=cbbaca.

Reduce LHS:

Referenced by [35].

Overlap of [6] ababc=bb with [28] cbbc=abba:

Critical pair: abababba=bbbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Referenced by [57], [58], [59].

Overlap of [28] cbbc=abba with [4] caab=baac:

Critical pair: cbbbaac=abbaaab.

Reduce RHS:

Defines rule #42.

Referenced by [71], [72].

Overlap of [28] cbbc=abba with [9] cabc=aaba:

Critical pair: cbbaaba=abbaabc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [33], [34], [38], [40], [47], [66].

Overlap of [6] ababc=bb with [32] abcc=cbca:

Critical pair: abcbca=bbc.

Referenced by [44], [45], [46].

Overlap of [32] abcc=cbca with [4] caab=baac:

Critical pair: abcbaac=cbcaaab.

Reduce RHS:

Defines rule #40.

Overlap of [15] ccbc=acba with [25] cacb=bacc:

Critical pair: ccbbacc=acbaacb.

Reduce RHS:

Defines rule #49.

Overlap of [16] accc=ccca with [25] cacb=bacc:

Critical pair: accbacc=cccaacb.

Reduce RHS:

Defines rule #47.

Overlap of [28] cbbc=abba with [25] cacb=bacc:

Critical pair: cbbbacc=abbaacb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [42].

Overlap of [32] abcc=cbca with [25] cacb=bacc:

Critical pair: abcbacc=cbcaacb.

Reduce RHS:

Defines rule #48.

Simplify [10] bbabc=abaca.

Reduce RHS:

Defines rule #20.

Referenced by [43], [79].

Overlap of [17] ababacba=bbcbc with [26] abac=cbaa:

Critical pair: abcbaaba=bbcbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [48], [49], [50], [67].

Overlap of [22] baacb=cbabc with [23] aacb=baca:

Critical pair: bbaca=cbabc.

Flip LHS and RHS.

Defines rule #19.

Referenced by [42], [47], [59], [72], [77].

Overlap of [37] abcbabc=cbbbacc with [41] cbabc=bbaca:

Critical pair: abbbaca=cbbbacc.

Flip LHS and RHS.

Defines rule #50.

Overlap of [39] bbabc=cb with [28] cbbc=abba:

Critical pair: bbababba=cbbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [55], [56], [68], [80].

Overlap of [6] ababc=bb with [33] abcbca=bbc:

Critical pair: abbbc=bbbca.

Defines rule #24.

Referenced by [53], [54], [69].

Overlap of [33] abcbca=bbc with [1] aaa=1:

Critical pair: abcbc=bbcaa.

Defines rule #21.

Overlap of [33] abcbca=bbc with [4] caab=baac:

Critical pair: abcbbaac=bbcab.

Defines rule #61.

Overlap of [32] abcc=cbca with [41] cbabc=bbaca:

Critical pair: abcbbaca=cbcababc.

Reduce RHS:

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

Overlap of [3] baab=c with [40] bbcbc=cbcaa:

Critical pair: baacbcaa=cbcbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

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

Overlap of [40] bbcbc=cbcaa with [4] caab=baac:

Critical pair: bbcbbaac=cbcaaaab.

Reduce RHS:

Defines rule #63.

Overlap of [40] bbcbc=cbcaa with [25] cacb=bacc:

Critical pair: bbcbbacc=cbcaaacb.

Reduce RHS:

Defines rule #72.

Overlap of [48] cbcbc=bbcca with [4] caab=baac:

Critical pair: cbcbbaac=bbccaaab.

Reduce RHS:

Defines rule #62.

Overlap of [48] cbcbc=bbcca with [25] cacb=bacc:

Critical pair: cbcbbacc=bbccaacb.

Reduce RHS:

Defines rule #71.

Overlap of [44] abbbc=bbbca with [4] caab=baac:

Critical pair: abbbbaac=bbbcaaab.

Reduce RHS:

Defines rule #64.

Overlap of [44] abbbc=bbbca with [25] cacb=bacc:

Critical pair: abbbbacc=bbbcaacb.

Reduce RHS:

Defines rule #73.

Overlap of [28] cbbc=abba with [43] cbbbc=bbbaa:

Critical pair: cbbbbbaa=abbabbbc.

Reduce RHS:

Referenced by [60].

Overlap of [43] cbbbc=bbbaa with [4] caab=baac:

Critical pair: cbbbbaac=bbbaaaab.

Reduce RHS:

Defines rule #65.

Referenced by [85].

Overlap of [30] bbbbc=abbaa with [4] caab=baac:

Critical pair: bbbbbaac=abbaaaab.

Reduce RHS:

Defines rule #66.

Overlap of [30] bbbbc=abbaa with [25] cacb=bacc:

Critical pair: bbbbbacc=abbaaacb.

Reduce RHS:

Defines rule #74.

Overlap of [30] bbbbc=abbaa with [41] cbabc=bbaca:

Critical pair: bbbbbbaca=abbaababc.

Reduce RHS:

Referenced by [81].

Overlap of [55] cbbbbbaa=ba with [1] aaa=1:

Critical pair: cbbbbb=baa.

Defines rule #36.

Referenced by [61], [62], [63], [64], [65], [66], [67], [68], [69], [70].

Overlap of [6] ababc=bb with [60] cbbbbb=baa:

Critical pair: ababbaa=bbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #60.

Overlap of [15] ccbc=acba with [60] cbbbbb=baa:

Critical pair: ccbbaa=acbabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [73], [75], [77].

Overlap of [16] accc=ccca with [60] cbbbbb=baa:

Critical pair: accbaa=cccabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #31.

Overlap of [26] abac=cbaa with [60] cbbbbb=baa:

Critical pair: ababaa=cbaabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #35.

Overlap of [28] cbbc=abba with [60] cbbbbb=baa:

Critical pair: cbbbaa=abbabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #28.

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

Overlap of [32] abcc=cbca with [60] cbbbbb=baa:

Critical pair: abcbaa=cbcabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #32.

Referenced by [67], [79].

Overlap of [40] bbcbc=cbcaa with [60] cbbbbb=baa:

Critical pair: bbcbbaa=cbcaabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #51.

Referenced by [83], [84], [86].

Overlap of [43] cbbbc=bbbaa with [60] cbbbbb=baa:

Critical pair: cbbbbaa=bbbaabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #58.

Overlap of [44] abbbc=bbbca with [60] cbbbbb=baa:

Critical pair: abbbbaa=bbbcabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #56.

Overlap of [48] cbcbc=bbcca with [60] cbbbbb=baa:

Critical pair: cbcbbaa=bbccabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #53.

Overlap of [11] aacc=caca with [31] cbbbaac=abbb:

Critical pair: aacabbb=cacabbbaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #45.

Overlap of [41] cbabc=bbaca with [31] cbbbaac=abbb:

Critical pair: cbababbb=bbacabbbaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #68.

Referenced by [86].

Overlap of [62] acabab=ccbbaa with [27] ababaac=cbab:

Critical pair: accbab=ccbbaaaac.

Reduce RHS:

Defines rule #29.

Referenced by [75], [76].

Overlap of [65] ababab=cbbbaa with [27] ababaac=cbab:

Critical pair: abcbab=cbbbaaaac.

Reduce RHS:

Defines rule #30.

Referenced by [77], [78].

Overlap of [11] aacc=caca with [73] accbab=ccbbac:

Critical pair: accbbac=cacabab.

Reduce RHS:

Defines rule #43.

Overlap of [73] accbab=ccbbac with [6] ababc=bb:

Critical pair: accbbb=ccbbacabc.

Reduce RHS:

Defines rule #33.

Overlap of [41] cbabc=bbaca with [74] abcbab=cbbbac:

Critical pair: cbcbbbac=bbacabab.

Reduce RHS:

Defines rule #67.

Overlap of [74] abcbab=cbbbac with [6] ababc=bb:

Critical pair: abcbbb=cbbbacabc.

Reduce RHS:

Defines rule #34.

Referenced by [80], [85].

Overlap of [39] bbabc=cb with [66] cbbbab=abcbaa:

Critical pair: bbababcbaa=cbbbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #55.

Referenced by [85], [87].

Overlap of [78] abcbbb=cbbbba with [43] cbbbc=bbbaa:

Critical pair: abbbbaa=cbbbbac.

Flip LHS and RHS.

Defines rule #46.

Referenced by [87].

Overlap of [59] bbbbbbaca=aca with [1] aaa=1:

Critical pair: bbbbbbac=acaaa.

Reduce RHS:

Defines rule #70.

Overlap of [47] abcbbaca=cbcbb with [1] aaa=1:

Critical pair: abcbbac=cbcbbaa.

Defines rule #44.

Overlap of [47] abcbbaca=cbcbb with [4] caab=baac:

Critical pair: abcbbabaac=cbcbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #52.

Overlap of [47] abcbbaca=cbcbb with [7] cabb=baba:

Critical pair: abcbbababa=cbcbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #57.

Overlap of [78] abcbbb=cbbbba with [56] cbbbbaac=bbbab:

Critical pair: abbbbab=cbbbbabaac.

Reduce RHS:

Defines rule #54.

Overlap of [5] babb=aaba with [72] bbcbbbac=cbbab:

Critical pair: babcbbab=aababcbbbac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #69.

Overlap of [80] cbbbbac=abbbbaa with [7] cabb=baba:

Critical pair: cbbbbababa=abbbbaaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #59.