Certificate for #3229 ⟨a, b | ababaaaabba=1⟩

Completion settings:

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

Axiom: ababaaaabba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #2.

Referenced by [4], [5], [7], [12], [17], [21], [26], [27], [34], [36], [39], [40], [41], [48], [51], [53], [55], [56], [62], [63], [66], [68], [69].

Axiom: bbaabab=d.

Defines rule #14.

Referenced by [6], [8], [13], [36], [45].

Overlap of [1] ababaaaabba=1 with [2] aaaa=c:

Critical pair: ababcbba=1.

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

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

Critical pair: ac=ca.

Defines rule #1.

Referenced by [21], [28], [35], [43], [52], [58], [59], [60].

Overlap of [3] bbaabab=d with [3] bbaabab=d:

Critical pair: bbaabad=dbaabab.

Flip LHS and RHS.

Referenced by [31].

Overlap of [2] aaaa=c with [4] ababcbba=1:

Critical pair: aaa=cbabcbba.

Flip LHS and RHS.

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

Overlap of [3] bbaabab=d with [4] ababcbba=1:

Critical pair: bba=dcbba.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: ababcbb=babcbba.

Referenced by [10].

Overlap of [4] ababcbba=1 with [9] ababcbb=babcbba:

Critical pair: babcbbaa=1.

Referenced by [11], [12], [13], [14].

Overlap of [8] dcbba=bba with [10] babcbbaa=1:

Critical pair: dcb=bbabcbbaa.

Reduce RHS:

Referenced by [14], [16], [18].

Overlap of [10] babcbbaa=1 with [2] aaaa=c:

Critical pair: babcbbc=aa.

Referenced by [20], [22].

Overlap of [10] babcbbaa=1 with [3] bbaabab=d:

Critical pair: babcd=bab.

Referenced by [15].

Overlap of [11] dcb=b with [10] babcbbaa=1:

Critical pair: dc=babcbbaa.

Reduce RHS:

Defines rule #3.

Referenced by [18], [22], [23], [26], [27], [29], [34], [44], [48], [49], [51], [52], [53], [54], [58], [65].

Overlap of [7] cbabcbba=aaa with [13] babcd=bab:

Critical pair: cbabcbbab=aaabcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [11] dcb=b with [7] cbabcbba=aaa:

Critical pair: daaa=babcbba.

Flip LHS and RHS.

Referenced by [19].

Overlap of [2] aaaa=c with [15] aaabcd=aaab:

Critical pair: aaaab=cbcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [11] dcb=b with [17] cbcd=cb:

Critical pair: dcb=bcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [7] cbabcbba=aaa with [16] babcbba=daaa:

Critical pair: cdaaa=aaa.

Referenced by [21], [24].

Overlap of [12] babcbbc=aa with [18] bcd=b:

Critical pair: babcbb=aad.

Referenced by [22], [30].

Overlap of [5] ac=ca with [19] cdaaa=aaa:

Critical pair: aaaa=cadaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [12] babcbbc=aa with [21] cadaaa=c:

Critical pair: babcbbc=aaadaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [14] dc=1 with [21] cadaaa=c:

Critical pair: dc=adaaa.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [19] cdaaa=aaa with [23] adaaa=1:

Critical pair: cdaa=aaadaaa.

Reduce RHS:

Referenced by [26].

Overlap of [23] adaaa=1 with [23] adaaa=1:

Critical pair: adaa=daaa.

Referenced by [26], [27].

Overlap of [24] cdaa=aa with [23] adaaa=1:

Critical pair: cda=aadaaa.

Reduce RHS:

Referenced by [27].

Overlap of [26] cda=a with [23] adaaa=1:

Critical pair: cd=adaaa.

Reduce RHS:

Defines rule #4.

Referenced by [28], [32], [36], [37], [42], [61], [67].

Overlap of [5] ac=ca with [27] cd=1:

Critical pair: a=cad.

Flip LHS and RHS.

Referenced by [29].

Overlap of [14] dc=1 with [28] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #5.

Referenced by [30], [31], [33], [49], [57], [61], [67].

Simplify [20] babcbb=aad.

Reduce RHS:

Referenced by [37].

Simplify [6] dbaabab=bbaabad.

Reduce RHS:

Defines rule #12.

Referenced by [32], [33], [46].

Overlap of [27] cd=1 with [31] dbaabab=bbaabda:

Critical pair: cbbaabda=baabab.

Referenced by [34].

Overlap of [29] ad=da with [31] dbaabab=bbaabda:

Critical pair: abbaabda=dabaabab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [49].

Overlap of [32] cbbaabda=baabab with [2] aaaa=c:

Critical pair: cbbaabdc=baababaaa.

Reduce LHS:

Defines rule #6.

Referenced by [35], [36], [41], [50].

Overlap of [5] ac=ca with [34] cbbaab=baababaaa:

Critical pair: abaababaaa=cabbaab.

Flip LHS and RHS.

Defines rule #9.

Overlap of [34] cbbaab=baababaaa with [3] bbaabab=d:

Critical pair: cd=baababaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [37], [38].

Overlap of [36] baababcb=1 with [30] babcbb=daa:

Critical pair: baababcdaa=abcbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [39], [52], [55], [62], [63], [68], [69].

Overlap of [36] baababcb=1 with [36] baababcb=1:

Critical pair: baababc=aababcb.

Flip LHS and RHS.

Referenced by [40].

Overlap of [2] aaaa=c with [37] abcbb=baababaa:

Critical pair: aaabaababaa=cbcbb.

Referenced by [43].

Overlap of [2] aaaa=c with [38] aababcb=baababc:

Critical pair: aabaababc=cbabcb.

Referenced by [41], [42].

Overlap of [34] cbbaab=baababaaa with [40] aabaababc=cbabcb:

Critical pair: cbbcbabcb=baababaaaaababc.

Reduce RHS:

Defines rule #16.

Overlap of [40] aabaababc=cbabcb with [27] cd=1:

Critical pair: aabaabab=cbabcbd.

Defines rule #11.

Referenced by [43], [47], [49], [53], [60].

Simplify [39] aaabaababaa=cbcbb.

Reduce LHS:

Referenced by [44].

Overlap of [14] dc=1 with [43] cababcbdaa=cbcbb:

Critical pair: dcbcbb=ababcbdaa.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [3] bbaabab=d with [44] ababcbdaa=bcbb:

Critical pair: bbaabbcbb=dabcbdaa.

Defines rule #27.

Overlap of [31] dbaabab=bbaabda with [44] ababcbdaa=bcbb:

Critical pair: dbaabbcbb=bbaabdaabcbdaa.

Defines rule #25.

Referenced by [57].

Overlap of [42] aabaabab=cbabcbd with [44] ababcbdaa=bcbb:

Critical pair: aabaabbcbb=cbabcbdabcbdaa.

Defines rule #24.

Overlap of [44] ababcbdaa=bcbb with [2] aaaa=c:

Critical pair: ababcbdc=bcbbaa.

Reduce LHS:

Defines rule #8.

Referenced by [55], [62], [63], [64], [68], [69].

Overlap of [29] ad=da with [33] dabaabab=abbaabda:

Critical pair: aabbaabda=daabaabab.

Reduce RHS:

Referenced by [50], [51].

Overlap of [34] cbbaab=baababaaa with [49] aabbaabda=babcbd:

Critical pair: cbbbabcbd=baababaaabaabda.

Referenced by [58].

Overlap of [49] aabbaabda=babcbd with [2] aaaa=c:

Critical pair: aabbaabdc=babcbdaaa.

Reduce LHS:

Defines rule #10.

Referenced by [52], [53].

Overlap of [51] aabbaab=babcbdaaa with [37] abcbb=baababaa:

Critical pair: aabbabaababaa=babcbdaaacbb.

Reduce RHS:

Referenced by [56].

Overlap of [51] aabbaab=babcbdaaa with [42] aabaabab=cbabcbd:

Critical pair: aabbcbabcbd=babcbdaaaaabab.

Reduce RHS:

Referenced by [54].

Overlap of [53] aabbcbabcbd=babcbabab with [14] dc=1:

Critical pair: aabbcbabcb=babcbababc.

Defines rule #22.

Referenced by [55].

Overlap of [2] aaaa=c with [54] aabbcbabcb=babcbababc:

Critical pair: aaababcbababc=cabbcbabcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [52] aabbabaababaa=babcbaaabb with [2] aaaa=c:

Critical pair: aabbabaababc=babcbaaabbaa.

Referenced by [61].

Overlap of [29] ad=da with [46] dbaabbcbb=bbaabdaabcbdaa:

Critical pair: abbaabdaabcbdaa=dabaabbcbb.

Flip LHS and RHS.

Defines rule #26.

Overlap of [50] cbbbabcbd=baababaaabaabda with [14] dc=1:

Critical pair: cbbbabcb=baababaaabaabdac.

Reduce RHS:

Defines rule #15.

Referenced by [59].

Overlap of [5] ac=ca with [58] cbbbabcb=baababaaabaaba:

Critical pair: abaababaaabaaba=cabbbabcb.

Flip LHS and RHS.

Defines rule #18.

Referenced by [60].

Overlap of [5] ac=ca with [59] cabbbabcb=abaababaaabaaba:

Critical pair: aabaababaaabaaba=caabbbabcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [65].

Overlap of [56] aabbabaababc=babcbaaabbaa with [27] cd=1:

Critical pair: aabbabaabab=babcbaaabbaad.

Reduce RHS:

Defines rule #23.

Referenced by [62], [63], [64].

Overlap of [2] aaaa=c with [61] aabbabaabab=babcbaaabbdaa:

Critical pair: aababcbaaabbdaa=cbbabaabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [2] aaaa=c with [61] aabbabaabab=babcbaaabbdaa:

Critical pair: aaababcbaaabbdaa=cabbabaabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [61] aabbabaabab=babcbaaabbdaa with [48] ababcb=bcbbaa:

Critical pair: aabbabaabbcbbaa=babcbaaabbdaaabcb.

Referenced by [66].

Overlap of [14] dc=1 with [60] caabbbabcb=cbabcbdaaabaaba:

Critical pair: dcbabcbdaaabaaba=aabbbabcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [64] aabbabaabbcbbaa=babcbaaabbdaaabcb with [2] aaaa=c:

Critical pair: aabbabaabbcbbc=babcbaaabbdaaabcbaa.

Referenced by [67].

Overlap of [66] aabbabaabbcbbc=babcbaaabbdaaabcbaa with [27] cd=1:

Critical pair: aabbabaabbcbb=babcbaaabbdaaabcbaad.

Reduce RHS:

Defines rule #30.

Referenced by [68], [69].

Overlap of [2] aaaa=c with [67] aabbabaabbcbb=babcbaaabbdaaabcbdaa:

Critical pair: aababcbaaabbdaaabcbdaa=cbbabaabbcbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [2] aaaa=c with [67] aabbabaabbcbb=babcbaaabbdaaabcbdaa:

Critical pair: aaababcbaaabbdaaabcbdaa=cabbabaabbcbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.