Certificate for #16582 ⟨a, b | aaaa=1, aababbb=1⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(b) = 0; deg(a) = 1

Axiom: aaaa=1.

Referenced by [3], [4].

Axiom: aababbb=1.

Referenced by [3], [4], [5], [6], [7], [8], [14].

Overlap of [1] aaaa=1 with [2] aababbb=1:

Critical pair: aa=babbb.

Defines rule #2.

Referenced by [4], [5], [6], [7], [8], [10], [14], [15], [17], [19], [35], [39].

Overlap of [1] aaaa=1 with [2] aababbb=1:

Critical pair: aaa=ababbb.

Reduce LHS:

Referenced by [7], [8], [10], [14], [15], [17], [19], [21].

Overlap of [2] aababbb=1 with [3] aa=babbb:

Critical pair: babbbbabbb=1.

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

Overlap of [2] aababbb=1 with [5] babbbbabbb=1:

Critical pair: aababb=abbbbabbb.

Reduce LHS:

Referenced by [7], [10], [14], [17], [18], [19], [20].

Overlap of [2] aababbb=1 with [4] babbba=ababbb:

Critical pair: aaababbb=a.

Reduce LHS:

Referenced by [8], [9], [12], [17], [28], [37], [40], [45].

Overlap of [2] aababbb=1 with [7] babbbbbbbabbbb=a:

Critical pair: aaa=bbbbabbbb.

Reduce LHS:

Referenced by [10], [11], [12], [14], [15], [16], [17], [19], [20].

Overlap of [7] babbbbbbbabbbb=a with [7] babbbbbbbabbbb=a:

Critical pair: babbbbbba=abbbabbbb.

Referenced by [14], [34], [36].

Overlap of [8] ababbb=bbbbabbbb with [4] babbba=ababbb:

Critical pair: aababbb=bbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20], [22].

Overlap of [8] ababbb=bbbbabbbb with [5] babbbbabbb=1:

Critical pair: a=bbbbabbbbbabbb.

Flip LHS and RHS.

Referenced by [12], [13].

Overlap of [8] ababbb=bbbbabbbb with [11] bbbbabbbbbabbb=a:

Critical pair: ababba=bbbbabbbbbbbabbbbbabbb.

Reduce RHS:

Referenced by [14].

Overlap of [11] bbbbabbbbbabbb=a with [11] bbbbabbbbbabbb=a:

Critical pair: bbbbaba=abbabbb.

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

Overlap of [2] aababbb=1 with [13] bbbbaba=abbabbb:

Critical pair: aababbabbabbb=bbbaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [13] bbbbaba=abbabbb with [3] aa=babbb:

Critical pair: bbbbabbabbb=abbabbba.

Reduce RHS:

Referenced by [24].

Overlap of [13] bbbbaba=abbabbb with [8] ababbb=bbbbabbbb:

Critical pair: bbbbbbbbabbbb=abbabbbbbb.

Flip LHS and RHS.

Referenced by [25].

Overlap of [4] babbba=ababbb with [6] babbbbabb=abbbbabbb:

Critical pair: babbabbbbabbb=ababbbbbbbabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [5] babbbbabbb=1 with [6] babbbbabb=abbbbabbb:

Critical pair: abbbbabbbb=1.

Referenced by [20], [22], [27].

Overlap of [6] babbbbabb=abbbbabbb with [6] babbbbabb=abbbbabbb:

Critical pair: babbbbababbbbabbb=abbbbabbbabbbbabb.

Reduce LHS:

Reduce RHS:

Referenced by [26].

Overlap of [8] ababbb=bbbbabbbb with [6] babbbbabb=abbbbabbb:

Critical pair: ababbabbbbabbb=bbbbabbbbabbbbabb.

Reduce LHS:

Reduce RHS:

Referenced by [21], [30], [31], [34].

Simplify [4] babbba=ababbb.

Reduce RHS:

Referenced by [29], [34], [35], [42].

Simplify [10] bbbbabbbba=abbbbabbbb.

Reduce RHS:

Referenced by [26].

Overlap of [13] bbbbaba=abbabbb with [14] bbbaba=bbbbbbbabbbbbbbbbbbbbbbbb:

Critical pair: bbbbbbbbabbbbbbbbbbbbbbbbb=abbabbb.

Flip LHS and RHS.

Referenced by [24], [25].

Overlap of [15] bbbbabbabbb=abbbbbabbbb with [23] abbabbb=bbbbbbbbabbbbbbbbbbbbbbbbb:

Critical pair: bbbbbbbbbbbbabbbbbbbbbbbbbbbbb=abbbbbabbbb.

Flip LHS and RHS.

Referenced by [26].

Overlap of [16] abbabbbbbb=bbbbbbbbabbbb with [23] abbabbb=bbbbbbbbabbbbbbbbbbbbbbbbb:

Critical pair: bbbbbbbbabbbbbbbbbbbbbbbbbbbb=bbbbbbbbabbbb.

Referenced by [26], [39].

Overlap of [19] bbabbbbbabbbbbbbabbb=abbbbab with [24] abbbbbabbbb=bbbbbbbbbbbbabbbbbbbbbbbbbbbbb:

Critical pair: bbbbbbbbbbbbbbabbbbbbbbbbbbbbbbbbbbabbb=abbbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27], [43].

Simplify [18] abbbbabbbb=1.

Reduce LHS:

Defines rule #1.

Referenced by [28], [29], [30], [33], [38], [42], [43], [44], [46], [48], [50], [51], [52], [53].

Overlap of [7] babbbbbbbabbbb=a with [27] bbbbbbbbbbbbbbbb=1:

Critical pair: babbbbbbba=abbbbbbbbbbbb.

Referenced by [33], [34], [48], [49].

Overlap of [27] bbbbbbbbbbbbbbbb=1 with [21] babbba=bbbbabbbb:

Critical pair: bbbbbbbbbbbbbbbbbbbabbbb=abbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [32], [36], [52].

Overlap of [20] abab=bbbbabb with [27] bbbbbbbbbbbbbbbb=1:

Critical pair: aba=bbbbabbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #3.

Referenced by [31], [32], [34], [35], [41], [49].

Overlap of [20] abab=bbbbabb with [30] aba=bbbbab:

Critical pair: abbbbbab=bbbbabba.

Flip LHS and RHS.

Referenced by [33], [34], [35], [42].

Overlap of [29] abbba=bbbabbbb with [30] aba=bbbbab:

Critical pair: abbbbbbbab=bbbabbbbba.

Flip LHS and RHS.

Referenced by [33], [34].

Overlap of [27] bbbbbbbbbbbbbbbb=1 with [31] bbbbabba=abbbbbab:

Critical pair: bbbbbbbbbbbbabbbbbab=abba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [39], [42].

Overlap of [20] abab=bbbbabb with [31] bbbbabba=abbbbbab:

Critical pair: abaabbbbbab=bbbbabbbbbabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [37], [40].

Overlap of [31] bbbbabba=abbbbbab with [3] aa=babbb:

Critical pair: bbbbabbbabbb=abbbbbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [50].

Simplify [9] babbbbbba=abbbabbbb.

Reduce RHS:

Referenced by [37], [38].

Overlap of [36] babbbbbba=bbbabbbbbbbb with [7] babbbbbbbabbbb=a:

Critical pair: babbbbba=bbbabbbbbbbbbbbbbbbabbbb.

Reduce RHS:

Referenced by [45].

Overlap of [27] bbbbbbbbbbbbbbbb=1 with [36] babbbbbba=bbbabbbbbbbb:

Critical pair: bbbbbbbbbbbbbbbbbbabbbbbbbb=abbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [39], [40], [41], [42], [44], [52].

Overlap of [3] aa=babbb with [38] abbbbbba=bbabbbbbbbb:

Critical pair: abbabbbbbbbb=babbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [38] abbbbbba=bbabbbbbbbb with [7] babbbbbbbabbbb=a:

Critical pair: abbbbba=bbabbbbbbbbbbbbbbbabbbb.

Reduce RHS:

Defines rule #7.

Overlap of [38] abbbbbba=bbabbbbbbbb with [30] aba=bbbbab:

Critical pair: abbbbbbbbbbab=bbabbbbbbbbba.

Reduce RHS:

Referenced by [53].

Overlap of [38] abbbbbba=bbabbbbbbbb with [31] bbbbabba=abbbbbab:

Critical pair: abbabbbbbab=bbabbbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [47].

Overlap of [26] abbbbab=bbbbbbbbbbbbb with [27] bbbbbbbbbbbbbbbb=1:

Critical pair: abbbba=bbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #6.

Referenced by [44], [51].

Overlap of [38] abbbbbba=bbabbbbbbbb with [43] abbbba=bbbbbbbbbbbb:

Critical pair: abbbbbbbbbbbbbbbbbb=bbabbbbbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [7] babbbbbbbabbbb=a with [44] bbabbbbbbbbbbbba=abb:

Critical pair: babbbbbabb=abbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [27] bbbbbbbbbbbbbbbb=1 with [44] bbabbbbbbbbbbbba=abb:

Critical pair: bbbbbbbbbbbbbbabb=abbbbbbbbbbbba.

Flip LHS and RHS.

Defines rule #14.

Overlap of [44] bbabbbbbbbbbbbba=abb with [44] bbabbbbbbbbbbbba=abb:

Critical pair: bbabbbbbbbbbbabb=abbbbbbbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [27] bbbbbbbbbbbbbbbb=1 with [28] babbbbbbba=abbbbbbbbbbbb:

Critical pair: bbbbbbbbbbbbbbbabbbbbbbbbbbb=abbbbbbba.

Flip LHS and RHS.

Defines rule #9.

Overlap of [28] babbbbbbba=abbbbbbbbbbbb with [30] aba=bbbbab:

Critical pair: babbbbbbbbbbbab=abbbbbbbbbbbbba.

Referenced by [54].

Overlap of [35] abbbbbbbbbab=bbbbbbbabbbbbbb with [27] bbbbbbbbbbbbbbbb=1:

Critical pair: abbbbbbbbba=bbbbbbbabbbbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #11.

Referenced by [51].

Overlap of [43] abbbba=bbbbbbbbbbbb with [50] abbbbbbbbba=bbbbbbbabbbbbb:

Critical pair: abbbbbbbbbbbabbbbbb=bbbbbbbbbbbbbbbbbbbbba.

Reduce RHS:

Referenced by [52].

Overlap of [38] abbbbbba=bbabbbbbbbb with [51] abbbbbbbbbbbabbbbbb=bbbbba:

Critical pair: abbbbbbbbbbba=bbabbbbbbbbbbbbbbbbbbbabbbbbb.

Reduce RHS:

Defines rule #13.

Referenced by [54].

Overlap of [41] abbbbbbbbbbab=bbbbbbbbbabbbbbb with [27] bbbbbbbbbbbbbbbb=1:

Critical pair: abbbbbbbbbba=bbbbbbbbbabbbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #12.

Simplify [49] babbbbbbbbbbbab=abbbbbbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.