Certificate for #3126 ⟨a, b | aabbabbaaba=1⟩

Completion settings:

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

Axiom: aabbabbaaba=1.

Referenced by [4].

Axiom: bb=c.

Defines rule #5.

Referenced by [3], [4], [5], [14], [16], [18], [23], [26], [27], [28], [32], [39], [44], [45], [53], [56], [58], [61], [62], [66], [67].

Axiom: abbaabaaa=d.

Reduce LHS:

Referenced by [7], [8], [9].

Overlap of [1] aabbabbaaba=1 with [2] bb=c:

Critical pair: aacabbaaba=1.

Reduce LHS:

Referenced by [6], [7], [8], [9], [10], [11], [13].

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

Critical pair: bc=cb.

Defines rule #3.

Referenced by [12], [26], [28], [36], [42], [50], [53], [55], [58], [61], [64], [66], [69].

Overlap of [4] aacacaaba=1 with [4] aacacaaba=1:

Critical pair: aacacaab=acacaaba.

Flip LHS and RHS.

Referenced by [7], [13], [26], [27].

Overlap of [3] acaabaaa=d with [4] aacacaaba=1:

Critical pair: acaabaa=dacacaaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [4] aacacaaba=1 with [3] acaabaaa=d:

Critical pair: aacd=aa.

Referenced by [10].

Overlap of [4] aacacaaba=1 with [3] acaabaaa=d:

Critical pair: aacacaabd=caabaaa.

Flip LHS and RHS.

Referenced by [25].

Overlap of [4] aacacaaba=1 with [8] aacd=aa:

Critical pair: aacacaabaa=acd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] aacacaaba=1 with [10] acd=a:

Critical pair: aacacaaba=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [12], [15], [16], [18], [20], [21], [24], [33], [48], [52], [57], [60], [63], [65], [68].

Overlap of [5] bc=cb with [11] cd=1:

Critical pair: b=cbd.

Flip LHS and RHS.

Referenced by [16].

Overlap of [4] aacacaaba=1 with [6] acacaaba=aacacaab:

Critical pair: aaacacaab=1.

Referenced by [14], [17].

Overlap of [13] aaacacaab=1 with [2] bb=c:

Critical pair: aaacacaac=b.

Referenced by [15], [16].

Overlap of [14] aaacacaac=b with [11] cd=1:

Critical pair: aaacacaa=bd.

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

Overlap of [14] aaacacaac=b with [12] cbd=b:

Critical pair: aaacacaab=bbd.

Reduce LHS:

Reduce RHS:

Referenced by [17], [22].

Overlap of [13] aaacacaab=1 with [16] bdb=1:

Critical pair: aaacacaa=db.

Reduce LHS:

Defines rule #4.

Referenced by [18], [19], [24], [25], [33], [35], [39], [48], [57], [63], [68].

Overlap of [2] bb=c with [17] bd=db:

Critical pair: bdb=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [26], [28], [31], [34], [36], [39], [40], [41], [44], [49], [53], [58], [61], [66].

Simplify [15] aaacacaa=bd.

Reduce RHS:

Defines rule #18.

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

Overlap of [19] aaacacaa=db with [19] aaacacaa=db:

Critical pair: aaacacdb=dbacacaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [11] cd=1 with [20] dbacacaa=aaacab:

Critical pair: caaacab=bacacaa.

Flip LHS and RHS.

Defines rule #12.

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

Overlap of [16] bdb=1 with [20] dbacacaa=aaacab:

Critical pair: baaacab=acacaa.

Referenced by [23].

Overlap of [22] baaacab=acacaa with [2] bb=c:

Critical pair: baaacac=acacaab.

Referenced by [24].

Overlap of [23] baaacac=acacaab with [11] cd=1:

Critical pair: baaaca=acacaabd.

Reduce RHS:

Defines rule #10.

Referenced by [28], [37], [53], [58], [61], [66].

Simplify [9] caabaaa=aacacaabd.

Reduce RHS:

Referenced by [34].

Overlap of [19] aaacacaa=db with [6] acacaaba=aacacaab:

Critical pair: aaacacaaacacaab=dbcacaaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [28], [29], [30], [38].

Overlap of [21] bacacaa=caaacab with [6] acacaaba=aacacaab:

Critical pair: baacacaab=caaacabba.

Reduce RHS:

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

Overlap of [2] bb=c with [26] bacaaba=aaacac:

Critical pair: baaacac=cacaaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [31], [51], [55].

Overlap of [26] bacaaba=aaacac with [21] bacacaa=caaacab:

Critical pair: bacaacaaacab=aaacaccacaa.

Referenced by [56].

Overlap of [26] bacaaba=aaacac with [26] bacaaba=aaacac:

Critical pair: bacaaaaacac=aaacaccaaba.

Referenced by [52].

Overlap of [18] dc=1 with [28] cacaaba=acacaab:

Critical pair: dacacaab=acaaba.

Referenced by [32].

Overlap of [31] dacacaab=acaaba with [2] bb=c:

Critical pair: dacacaac=acaabab.

Referenced by [33].

Overlap of [32] dacacaac=acaabab with [11] cd=1:

Critical pair: dacacaa=acaababd.

Reduce RHS:

Defines rule #8.

Overlap of [18] dc=1 with [25] caabaaa=aacacaadb:

Critical pair: daacacaadb=aabaaa.

Referenced by [35], [44].

Overlap of [7] daacacaab=acaabaa with [17] bd=db:

Critical pair: daacacaadb=acaabaad.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [19] aaacacaa=db with [35] acaabaad=aabaaa:

Critical pair: aaacacaaabaaa=dbcaabaad.

Reduce LHS:

Reduce RHS:

Defines rule #14.

Referenced by [39].

Overlap of [24] baaaca=acacaadb with [35] acaabaad=aabaaa:

Critical pair: baaaabaaa=acacaadbabaad.

Defines rule #23.

Overlap of [26] bacaaba=aaacac with [35] acaabaad=aabaaa:

Critical pair: baabaaa=aaacacad.

Defines rule #17.

Referenced by [43].

Overlap of [17] bd=db with [36] dbabaaa=baabaad:

Critical pair: bbaabaad=dbbabaaa.

Reduce LHS:

Reduce RHS:

Referenced by [40], [41].

Overlap of [18] dc=1 with [39] caabaad=abaaa:

Critical pair: dabaaa=aabaad.

Defines rule #9.

Overlap of [39] caabaad=abaaa with [18] dc=1:

Critical pair: caabaa=abaaac.

Defines rule #6.

Referenced by [42], [43], [46], [54], [59].

Overlap of [5] bc=cb with [41] caabaa=abaaac:

Critical pair: babaaac=cbaabaa.

Flip LHS and RHS.

Defines rule #13.

Referenced by [47].

Overlap of [41] caabaa=abaaac with [38] baabaaa=aaacacad:

Critical pair: caaaaacacad=abaaacbaaa.

Referenced by [49].

Overlap of [34] daacacaadb=aabaaa with [2] bb=c:

Critical pair: daacacaadc=aabaaab.

Reduce LHS:

Defines rule #15.

Overlap of [27] baacacaab=caaacaca with [2] bb=c:

Critical pair: baacacaac=caaacacab.

Referenced by [48].

Overlap of [41] caabaa=abaaac with [27] baacacaab=caaacaca:

Critical pair: caacaaacaca=abaaaccacaab.

Defines rule #20.

Referenced by [55].

Overlap of [42] cbaabaa=babaaac with [27] baacacaab=caaacaca:

Critical pair: cbaacaaacaca=babaaaccacaab.

Defines rule #27.

Overlap of [45] baacacaac=caaacacab with [11] cd=1:

Critical pair: baacacaa=caaacacabd.

Reduce RHS:

Defines rule #16.

Overlap of [43] caaaaacacad=abaaacbaaa with [18] dc=1:

Critical pair: caaaaacaca=abaaacbaaac.

Defines rule #19.

Referenced by [50], [51].

Overlap of [5] bc=cb with [49] caaaaacaca=abaaacbaaac:

Critical pair: babaaacbaaac=cbaaaaacaca.

Flip LHS and RHS.

Defines rule #26.

Overlap of [49] caaaaacaca=abaaacbaaac with [28] cacaaba=acacaab:

Critical pair: caaaaacaacacaab=abaaacbaaaccaaba.

Referenced by [62].

Overlap of [30] bacaaaaacac=aaacaccaaba with [11] cd=1:

Critical pair: bacaaaaaca=aaacaccaabad.

Defines rule #24.

Referenced by [53], [54].

Overlap of [2] bb=c with [52] bacaaaaaca=aaacaccaabad:

Critical pair: baaacaccaabad=cacaaaaaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [52] bacaaaaaca=aaacaccaabad with [41] caabaa=abaaac:

Critical pair: bacaaaaaabaaac=aaacaccaabadabaa.

Referenced by [60].

Overlap of [46] caacaaacaca=abaaaccacaab with [28] cacaaba=acacaab:

Critical pair: caacaaacaacacaab=abaaaccacaabcaaba.

Reduce RHS:

Referenced by [67].

Overlap of [29] bacaacaaacab=aaacaccacaa with [2] bb=c:

Critical pair: bacaacaaacac=aaacaccacaab.

Referenced by [57].

Overlap of [56] bacaacaaacac=aaacaccacaab with [11] cd=1:

Critical pair: bacaacaaaca=aaacaccacaabd.

Reduce RHS:

Defines rule #25.

Referenced by [58], [59].

Overlap of [2] bb=c with [57] bacaacaaaca=aaacaccacaadb:

Critical pair: baaacaccacaadb=cacaacaaaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [57] bacaacaaaca=aaacaccacaadb with [41] caabaa=abaaac:

Critical pair: bacaacaaaabaaac=aaacaccacaadbabaa.

Referenced by [65].

Overlap of [54] bacaaaaaabaaac=aaacaccaabadabaa with [11] cd=1:

Critical pair: bacaaaaaabaaa=aaacaccaabadabaad.

Defines rule #32.

Referenced by [61].

Overlap of [2] bb=c with [60] bacaaaaaabaaa=aaacaccaabadabaad:

Critical pair: baaacaccaabadabaad=cacaaaaaabaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #30.

Overlap of [51] caaaaacaacacaab=abaaacbaaaccaaba with [2] bb=c:

Critical pair: caaaaacaacacaac=abaaacbaaaccaabab.

Referenced by [63].

Overlap of [62] caaaaacaacacaac=abaaacbaaaccaabab with [11] cd=1:

Critical pair: caaaaacaacacaa=abaaacbaaaccaababd.

Reduce RHS:

Defines rule #28.

Referenced by [64].

Overlap of [5] bc=cb with [63] caaaaacaacacaa=abaaacbaaaccaabadb:

Critical pair: babaaacbaaaccaabadb=cbaaaaacaacacaa.

Flip LHS and RHS.

Defines rule #34.

Overlap of [59] bacaacaaaabaaac=aaacaccacaadbabaa with [11] cd=1:

Critical pair: bacaacaaaabaaa=aaacaccacaadbabaad.

Defines rule #33.

Referenced by [66].

Overlap of [2] bb=c with [65] bacaacaaaabaaa=aaacaccacaadbabaad:

Critical pair: baaacaccacaadbabaad=cacaacaaaabaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #31.

Overlap of [55] caacaaacaacacaab=abaaaccacaacbaaba with [2] bb=c:

Critical pair: caacaaacaacacaac=abaaaccacaacbaabab.

Referenced by [68].

Overlap of [67] caacaaacaacacaac=abaaaccacaacbaabab with [11] cd=1:

Critical pair: caacaaacaacacaa=abaaaccacaacbaababd.

Reduce RHS:

Defines rule #29.

Referenced by [69].

Overlap of [5] bc=cb with [68] caacaaacaacacaa=abaaaccacaacbaabadb:

Critical pair: babaaaccacaacbaabadb=cbaacaaacaacacaa.

Flip LHS and RHS.

Defines rule #35.