Certificate for #7519 ⟨a, b | aaa=1, ababba=b⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #11.

Referenced by [3], [4], [7], [11], [15], [20], [21], [22], [23], [24], [26], [27], [28], [30], [32], [36], [37], [41].

Axiom: ababba=b.

Referenced by [3], [4], [12], [14], [17].

Overlap of [1] aaa=1 with [2] ababba=b:

Critical pair: aab=babba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [5], [6], [8], [9], [10], [13], [21], [22], [24], [28], [30].

Overlap of [2] ababba=b with [1] aaa=1:

Critical pair: ababb=baa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6], [9], [10], [12], [13], [14], [16], [22], [25], [29], [30], [38].

Overlap of [3] babba=aab with [3] babba=aab:

Critical pair: babaab=aabbba.

Reduce LHS:

Referenced by [7], [16].

Overlap of [3] babba=aab with [4] baa=ababb:

Critical pair: babababb=aaba.

Referenced by [9], [15], [17], [22].

Overlap of [1] aaa=1 with [5] ababbbabbb=aabbba:

Critical pair: aaaabbba=babbbabbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9], [10], [22], [29], [30], [33].

Overlap of [3] babba=aab with [7] babbbabbb=abbba:

Critical pair: bababbba=aabbbbabbb.

Referenced by [9], [14], [15], [16], [17], [23], [24].

Overlap of [7] babbbabbb=abbba with [6] babababb=aaba:

Critical pair: babbbabbaaba=abbbaabababb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [7] babbbabbb=abbba with [7] babbbabbb=abbba:

Critical pair: babbabbba=abbbaabbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [1] aaa=1 with [10] abbababbbbb=aabbbba:

Critical pair: aaaabbbba=bbababbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [25], [28], [29], [30].

Overlap of [2] ababba=b with [10] abbababbbbb=aabbbba:

Critical pair: abaabbbba=bbabbbbb.

Reduce LHS:

Referenced by [14], [19].

Overlap of [3] babba=aab with [10] abbababbbbb=aabbbba:

Critical pair: baabbbba=aabbabbbbb.

Reduce LHS:

Referenced by [22], [29], [36].

Overlap of [2] ababba=b with [8] bababbba=aabbbbabbb:

Critical pair: ababaabbbbabbb=bbabbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [6] babababb=aaba with [8] bababbba=aabbbbabbb:

Critical pair: baaabbbbabbb=aababa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [20], [21], [22], [23].

Overlap of [8] bababbba=aabbbbabbb with [5] ababbbabbb=aabbba:

Critical pair: baabbba=aabbbbabbbbbb.

Reduce LHS:

Referenced by [29].

Overlap of [8] bababbba=aabbbbabbb with [11] bbababbbbb=abbbba:

Critical pair: babababbbba=aabbbbabbbbabbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Simplify [9] aababbbbbbabbbbabb=aabababa.

Reduce RHS:

Referenced by [19].

Overlap of [18] aababbbbbbabbbbabb=bbbbbabbbba with [12] aababbbbbba=bbabbbbb:

Critical pair: bbabbbbbbbbbabb=bbbbbabbbba.

Flip LHS and RHS.

Referenced by [22].

Overlap of [1] aaa=1 with [15] aababa=bbbbbabbb:

Critical pair: abbbbbabbb=baba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [24], [25], [30], [38].

Overlap of [15] aababa=bbbbbabbb with [3] babba=aab:

Critical pair: aabaaab=bbbbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25], [26].

Overlap of [15] aababa=bbbbbabbb with [6] babababb=aaba:

Critical pair: aabaaaba=bbbbbabbbbababb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [15] aababa=bbbbbabbb with [8] bababbba=aabbbbabbb:

Critical pair: aaaabbbbabbb=bbbbbabbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [8] bababbba=aabbbbabbb with [20] baba=abbbbbabbb:

Critical pair: bababbabbbbbabbb=aabbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25], [31].

Overlap of [11] bbababbbbb=abbbba with [21] bbbbbabbbbba=aabb:

Critical pair: bbababbbbaabb=abbbbabbbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [21] bbbbbabbbbba=aabb with [21] bbbbbabbbbba=aabb:

Critical pair: bbbbbaaabb=aabbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [1] aaa=1 with [26] aabbbbbbba=bbbbbbb:

Critical pair: abbbbbbb=bbbbbbba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [28], [29], [31], [34], [38].

Overlap of [11] bbababbbbb=abbbba with [27] bbbbbbba=abbbbbbb:

Critical pair: bbababbabbbbbbb=abbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [35], [37].

Overlap of [11] bbababbbbb=abbbba with [27] bbbbbbba=abbbbbbb:

Critical pair: bbababbbabbbbbbb=abbbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [7] babbbabbb=abbba with [29] abbbbabbbbba=aabbab:

Critical pair: babbbaabbab=abbbababbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [40].

Simplify [17] aabbbbabbbbabbbbb=ab.

Reduce LHS:

Referenced by [32], [33].

Overlap of [1] aaa=1 with [31] abbbbbbbbbbbbbbb=ab:

Critical pair: aaab=bbbbbbbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [35].

Overlap of [7] babbbabbb=abbba with [31] abbbbbbbbbbbbbbb=ab:

Critical pair: babbbab=abbbabbbbbbbbbbbb.

Referenced by [42].

Simplify [25] abbbbabbbbabbbbba=bbbbbbbbabbbbbbb.

Reduce RHS:

Referenced by [35].

Overlap of [34] abbbbabbbbabbbbba=babbbbbbbbbbbbbb with [28] abbbbabbbba=bbbbbbbbbb:

Critical pair: bbbbbbbbbbbbbbba=babbbbbbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [38], [39], [40], [42].

Overlap of [1] aaa=1 with [13] ababbbbbba=aabbabbbbb:

Critical pair: aaaabbabbbbb=babbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [1] aaa=1 with [28] abbbbabbbba=bbbbbbbbbb:

Critical pair: aabbbbbbbbbb=bbbbabbbba.

Flip LHS and RHS.

Referenced by [38].

Overlap of [27] bbbbbbba=abbbbbbb with [37] bbbbabbbba=aabbbbbbbbbb:

Critical pair: bbbaabbbbbbbbbb=abbbbbbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [39].

Overlap of [38] babbbbbab=abbbbabbbbbbb with [35] babbbbbbbbbbbbbb=ba:

Critical pair: babbbbba=abbbbabbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #8.

Overlap of [30] aabbabbbbab=bbbbbbabbbbb with [35] babbbbbbbbbbbbbb=ba:

Critical pair: aabbabbbba=bbbbbbabbbbbbbbbbbbbbbbbb.

Reduce RHS:

Referenced by [41].

Overlap of [1] aaa=1 with [40] aabbabbbba=bbbbbbabbbb:

Critical pair: abbbbbbabbbb=bbabbbba.

Flip LHS and RHS.

Defines rule #10.

Overlap of [33] babbbab=abbbabbbbbbbbbbbb with [35] babbbbbbbbbbbbbb=ba:

Critical pair: babbba=abbbabbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #7.