Certificate for #4169 ⟨a, b | aabbaabba=ba⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(a) = 0; deg(c) = 1; deg(b) = 2
• Auxiliary generators:
  1. bbbbbba=c

Axiom: aabbaabba=ba.

Referenced by [3], [4], [5], [6], [16].

Axiom: bbbbbba=c.

Referenced by [4], [15], [24], [25], [26], [27], [38].

Overlap of [1] aabbaabba=ba with [1] aabbaabba=ba:

Critical pair: aabbba=baabba.

Flip LHS and RHS.

Referenced by [4], [5], [6], [7], [8], [9], [10], [16], [29], [39].

Overlap of [2] bbbbbba=c with [1] aabbaabba=ba:

Critical pair: bbbbbbba=cabbaabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [5], [8], [11], [13], [15], [17].

Overlap of [4] cabaabbba=bc with [1] aabbaabba=ba:

Critical pair: cabaabbbba=bcabbaabba.

Reduce RHS:

Referenced by [11], [13], [18].

Overlap of [3] baabba=aabbba with [1] aabbaabba=ba:

Critical pair: bba=aabbbaabba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [7], [9], [12], [19].

Overlap of [3] baabba=aabbba with [3] baabba=aabbba:

Critical pair: baabaabbba=aabbbaabba.

Reduce RHS:

Referenced by [10], [11], [12], [14], [15].

Overlap of [4] cabaabbba=bc with [3] baabba=aabbba:

Critical pair: cabaabbaabbba=bcabba.

Reduce LHS:

Referenced by [20].

Overlap of [3] baabba=aabbba with [6] aabbaabbba=bba:

Critical pair: bbba=aabbbaabbba.

Flip LHS and RHS.

Referenced by [20].

Overlap of [3] baabba=aabbba with [7] baabaabbba=bba:

Critical pair: baabbba=aabbbaabaabbba.

Reduce RHS:

Referenced by [13], [14], [16], [17], [19], [24], [29], [30], [40].

Overlap of [5] cabaabbbba=bbc with [7] baabaabbba=bba:

Critical pair: cabaabbbbba=bbcabaabbba.

Reduce RHS:

Referenced by [15], [37].

Overlap of [6] aabbaabbba=bba with [7] baabaabbba=bba:

Critical pair: aabbaabbbba=bbaabaabbba.

Reduce RHS:

Referenced by [21].

Overlap of [5] cabaabbbba=bbc with [10] baabbba=aabbbba:

Critical pair: cabaabbbaabbbba=bbcabbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [10] baabbba=aabbbba with [7] baabaabbba=bba:

Critical pair: baabbbba=aabbbbaabaabbba.

Reduce RHS:

Referenced by [18], [19], [21], [29], [30], [42].

Overlap of [11] cabaabbbbba=bbbc with [7] baabaabbba=bba:

Critical pair: cabaabbbbbba=bbbcabaabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [22], [32], [37], [44].

Overlap of [1] aabbaabba=ba with [3] baabba=aabbba:

Critical pair: aabaabbba=ba.

Reduce LHS:

Referenced by [23], [25], [46].

Overlap of [4] cabaabbba=bc with [10] baabbba=aabbbba:

Critical pair: caaabbbba=bc.

Referenced by [22], [26], [32], [34], [47].

Overlap of [5] cabaabbbba=bbc with [14] baabbbba=aabbbbba:

Critical pair: caaabbbbba=bbc.

Referenced by [26], [28], [31], [36].

Overlap of [6] aabbaabbba=bba with [10] baabbba=aabbbba:

Critical pair: aabaabbbba=bba.

Reduce LHS:

Referenced by [24], [25], [26], [27], [28], [31], [48].

Overlap of [8] caaabbbaabbba=bcabba with [9] aabbbaabbba=bbba:

Critical pair: cabbba=bcabba.

Flip LHS and RHS.

Referenced by [23], [28], [33], [49].

Overlap of [12] aabbaabbbba=bbba with [14] baabbbba=aabbbbba:

Critical pair: aabaabbbbba=bbba.

Referenced by [37].

Overlap of [15] bbbbc=cabaac with [17] caaabbbba=bc:

Critical pair: bbbbbc=cabaacaaabbbba.

Reduce LHS:

Reduce RHS:

Referenced by [37].

Overlap of [20] bcabba=cabbba with [16] aaaabbbba=ba:

Critical pair: bcabbba=cabbbaaaabbbba.

Reduce RHS:

Referenced by [50].

Overlap of [10] baabbba=aabbbba with [19] aaaabbbbba=bba:

Critical pair: baabbbbba=aabbbbaaaabbbbba.

Reduce RHS:

Referenced by [30].

Overlap of [16] aaaabbbba=ba with [19] aaaabbbbba=bba:

Critical pair: aaaabbbbbba=baaaabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [27], [28], [29], [30], [31], [33], [35], [36], [37], [38], [39], [40], [41], [42], [43], [46], [47], [48], [49], [50], [51], [60].

Overlap of [17] caaabbbba=bc with [19] aaaabbbbba=bba:

Critical pair: caaabbbbbba=bcaaabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [19] aaaabbbbba=bba with [19] aaaabbbbba=bba:

Critical pair: aaaabbbbbbba=bbaaaabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [28], [29], [31], [33], [35], [36], [37], [40], [42], [43], [46], [47], [48], [50], [55], [56], [57].

Overlap of [20] bcabba=cabbba with [19] aaaabbbbba=bba:

Critical pair: bcabbbba=cabbbaaaabbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [33].

Overlap of [25] bbba=aaaac with [3] baabba=aabbba:

Critical pair: bbaabbba=aaaacabba.

Reduce LHS:

Referenced by [36], [42], [48].

Overlap of [25] bbba=aaaac with [10] baabbba=aabbbba:

Critical pair: bbaabbbba=aaaacabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [52], [55].

Overlap of [25] bbba=aaaac with [19] aaaabbbbba=bba:

Critical pair: bbbbba=aaaacaaabbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [35], [37], [52].

Overlap of [26] bbbc=caaac with [17] caaabbbba=bc:

Critical pair: bbbbc=caaacaaabbbba.

Reduce LHS:

Reduce RHS:

Referenced by [34], [44], [63].

Overlap of [26] bbbc=caaac with [20] bcabba=cabbba:

Critical pair: bbcabbba=caaacabba.

Reduce LHS:

Referenced by [37].

Overlap of [32] cabaac=caaabc with [17] caaabbbba=bc:

Critical pair: cabaabc=caaabcaaabbbba.

Reduce RHS:

Referenced by [37], [53].

Overlap of [25] bbba=aaaac with [27] baaaac=aaaabc:

Critical pair: bbaaaabc=aaaacaaac.

Reduce LHS:

Referenced by [54].

Simplify [18] caaabbbbba=bbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37], [52], [53], [55], [65].

Overlap of [36] bbc=caaaaacabba with [11] cabaabbbbba=bbbc:

Critical pair: bbbbbc=caaaaacabbaabaabbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [53].

Overlap of [2] bbbbbba=c with [25] bbba=aaaac:

Critical pair: bbbaaaac=c.

Reduce LHS:

Referenced by [53], [54], [56], [58], [59], [67].

Simplify [3] baabba=aabbba.

Reduce RHS:

Defines rule #20.

Referenced by [64].

Simplify [10] baabbba=aabbbba.

Reduce RHS:

Referenced by [41].

Overlap of [40] baabbba=aaaaaabc with [25] bbba=aaaac:

Critical pair: baaaaaac=aaaaaabc.

Defines rule #11.

Simplify [14] baabbbba=aabbbbba.

Reduce RHS:

Referenced by [43].

Overlap of [42] baabbbba=aaaacabba with [25] bbba=aaaac:

Critical pair: baabaaaac=aaaacabba.

Reduce LHS:

Defines rule #17.

Simplify [15] bbbbc=cabaac.

Reduce RHS:

Referenced by [45].

Overlap of [44] bbbbc=caaabc with [26] bbbc=caaac:

Critical pair: bcaaac=caaabc.

Referenced by [56], [63].

Overlap of [16] aaaabbbba=ba with [25] bbba=aaaac:

Critical pair: aaaabaaaac=ba.

Reduce LHS:

Defines rule #4.

Referenced by [60].

Overlap of [17] caaabbbba=bc with [25] bbba=aaaac:

Critical pair: caaabaaaac=bc.

Reduce LHS:

Defines rule #8.

Referenced by [60], [62], [70].

Overlap of [19] aaaabbbbba=bba with [25] bbba=aaaac:

Critical pair: aaaabbaaaac=bba.

Reduce LHS:

Defines rule #13.

Simplify [20] bcabba=cabbba.

Reduce RHS:

Referenced by [55], [60], [66].

Simplify [23] bcabbba=cabbbba.

Reduce RHS:

Referenced by [51].

Overlap of [50] bcabbba=caaaaabc with [25] bbba=aaaac:

Critical pair: bcaaaaac=caaaaabc.

Referenced by [55], [57], [60].

Simplify [31] baaaabc=aaaabbc.

Reduce RHS:

Defines rule #16.

Simplify [34] cabaabc=caaabbc.

Reduce RHS:

Referenced by [71].

Simplify [35] baaaabbc=aaaacaaac.

Reduce RHS:

Referenced by [55].

Overlap of [54] baaaabbc=c with [36] bbc=caaaaacabba:

Critical pair: baaaacaaaaacabba=c.

Reduce LHS:

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

Overlap of [27] baaaac=aaaabc with [38] aaaacaaac=c:

Critical pair: bc=aaaabcaaac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [61], [63].

Overlap of [27] baaaac=aaaabc with [55] aacaaaaac=c:

Critical pair: baac=aaaabcaaaaac.

Reduce RHS:

Referenced by [68].

Overlap of [38] aaaacaaac=c with [55] aacaaaaac=c:

Critical pair: aaaacac=caaaaac.

Flip LHS and RHS.

Defines rule #3.

Referenced by [60], [65], [66].

Overlap of [55] aacaaaaac=c with [38] aaaacaaac=c:

Critical pair: aacac=caaac.

Flip LHS and RHS.

Defines rule #2.

Referenced by [63], [67].

Overlap of [49] bcabba=caaaaac with [46] aaaaaaaabc=ba:

Critical pair: bcabbba=caaaaacaaaaaaabc.

Reduce LHS:

Reduce RHS:

Defines rule #7.

Referenced by [62], [68].

Overlap of [55] aacaaaaac=c with [56] aaaacaaabc=bc:

Critical pair: aacabc=caaabc.

Flip LHS and RHS.

Defines rule #6.

Referenced by [63].

Overlap of [55] aacaaaaac=c with [47] caaaaaaabc=bc:

Critical pair: aacaaaaabc=caaaaaaabc.

Reduce LHS:

Reduce RHS:

Defines rule #5.

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

Overlap of [62] aaaaaacabc=bc with [59] caaac=aacac:

Critical pair: aaaaaacabaacac=bcaaac.

Reduce LHS:

Reduce RHS:

Referenced by [64].

Overlap of [39] baabba=aaaaaac with [63] aabcac=aacabc:

Critical pair: baabbaacabc=aaaaaacabcac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [69].

Simplify [36] bbc=caaaaacabba.

Reduce RHS:

Defines rule #14.

Referenced by [70], [71].

Simplify [49] bcabba=caaaaac.

Reduce RHS:

Defines rule #21.

Overlap of [38] aaaacaaac=c with [59] caaac=aacac:

Critical pair: aaaaaacac=c.

Defines rule #1.

Referenced by [69], [70].

Simplify [57] baac=aaaacaaaaabc.

Reduce RHS:

Defines rule #9.

Referenced by [70], [71].

Simplify [64] bcac=aaaaaacacabc.

Reduce RHS:

Defines rule #12.

Referenced by [71].

Overlap of [68] baac=aabc with [47] caaaaaaabc=bc:

Critical pair: baabc=aabcaaaaaaabc.

Reduce RHS:

Defines rule #15.

Overlap of [65] bbc=aaaacacabba with [69] bcac=cabc:

Critical pair: bcabc=aaaacacabbaac.

Reduce RHS:

Defines rule #18.