Certificate for #23303 ⟨a, b | aaa=1, baba=abbb⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #13.

Referenced by [3], [5], [15], [19], [23], [24], [39], [45], [51], [53], [54].

Axiom: baba=abbb.

Defines rule #8.

Referenced by [3], [4], [6], [7], [10], [11], [13], [18], [20], [22], [28], [49].

Overlap of [2] baba=abbb with [1] aaa=1:

Critical pair: bab=abbbaa.

Flip LHS and RHS.

Defines rule #15.

Referenced by [5], [6], [7], [8], [9], [35], [45], [50], [52].

Overlap of [2] baba=abbb with [2] baba=abbb:

Critical pair: baabbb=abbbba.

Defines rule #7.

Referenced by [9], [10], [11], [16], [20], [21], [23], [25], [31], [32], [33], [45], [46], [54].

Overlap of [1] aaa=1 with [3] abbbaa=bab:

Critical pair: aabab=bbbaa.

Defines rule #14.

Referenced by [8], [20], [23], [25].

Overlap of [2] baba=abbb with [3] abbbaa=bab:

Critical pair: babbab=abbbbbbaa.

Flip LHS and RHS.

Defines rule #16.

Referenced by [17], [29], [34], [47].

Overlap of [3] abbbaa=bab with [3] abbbaa=bab:

Critical pair: abbbabab=babbbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12], [30], [35].

Overlap of [5] aabab=bbbaa with [3] abbbaa=bab:

Critical pair: aabbab=bbbaabbaa.

Flip LHS and RHS.

Defines rule #20.

Referenced by [11], [35], [48].

Overlap of [3] abbbaa=bab with [4] baabbb=abbbba:

Critical pair: abbabbbba=babbbb.

Referenced by [12], [14].

Overlap of [4] baabbb=abbbba with [2] baba=abbb:

Critical pair: baabbabbb=abbbbaaba.

Flip LHS and RHS.

Defines rule #19.

Referenced by [19].

Overlap of [4] baabbb=abbbba with [8] bbbaabbaa=aabbab:

Critical pair: baabaabbab=abbbbabaabbaa.

Reduce RHS:

Referenced by [36].

Overlap of [9] abbabbbba=babbbb with [7] babbbbaa=abbabbbb:

Critical pair: ababbabbbb=babbbba.

Referenced by [13], [20].

Overlap of [2] baba=abbb with [12] ababbabbbb=babbbba:

Critical pair: bbabbbba=abbbbbabbbb.

Referenced by [14], [20], [21], [23], [25], [28], [32].

Overlap of [9] abbabbbba=babbbb with [13] bbabbbba=abbbbbabbbb:

Critical pair: aabbbbbabbbb=babbbb.

Referenced by [15], [16], [17], [21], [24], [26], [37].

Overlap of [1] aaa=1 with [14] aabbbbbabbbb=babbbb:

Critical pair: ababbbb=bbbbbabbbb.

Referenced by [18], [22].

Overlap of [4] baabbb=abbbba with [14] aabbbbbabbbb=babbbb:

Critical pair: bbabbbb=abbbbabbabbbb.

Flip LHS and RHS.

Referenced by [20], [30].

Overlap of [14] aabbbbbabbbb=babbbb with [6] abbbbbbaa=babbab:

Critical pair: aabbbbbbabbab=babbbbbbaa.

Reduce RHS:

Referenced by [38].

Overlap of [2] baba=abbb with [15] ababbbb=bbbbbabbbb:

Critical pair: bbbbbbabbbb=abbbbbbb.

Referenced by [20], [21], [22], [24], [25], [27], [31], [39], [40].

Overlap of [1] aaa=1 with [10] abbbbaaba=baabbabbb:

Critical pair: aabaabbabbb=bbbbaaba.

Defines rule #22.

Referenced by [54].

Overlap of [12] ababbabbbb=babbbba with [18] bbbbbbabbbb=abbbbbbb:

Critical pair: ababbaabbbbbbb=babbbbabbabbbb.

Reduce LHS:

Reduce RHS:

Referenced by [21].

Overlap of [14] aabbbbbabbbb=babbbb with [18] bbbbbbabbbb=abbbbbbb:

Critical pair: aabbbbbaabbbbbbb=babbbbbbabbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [23], [24], [25], [31], [32], [33].

Overlap of [15] ababbbb=bbbbbabbbb with [18] bbbbbbabbbb=abbbbbbb:

Critical pair: abababbbbbbb=bbbbbabbbbbbbabbbb.

Reduce LHS:

Reduce RHS:

Referenced by [26].

Overlap of [1] aaa=1 with [21] abbbbabbbb=babbbbb:

Critical pair: aababbbbb=bbbbabbbb.

Reduce LHS:

Referenced by [28], [32].

Overlap of [14] aabbbbbabbbb=babbbb with [21] abbbbabbbb=babbbbb:

Critical pair: aabbbbbbabbbbb=babbbbabbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [25], [26], [27], [28], [29], [30], [31], [33], [35].

Overlap of [5] aabab=bbbaa with [24] bbabbbbb=bbbbbbbb:

Critical pair: aababbbbbbbb=bbbaababbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [26], [27], [30], [31].

Overlap of [14] aabbbbbabbbb=babbbb with [24] bbabbbbb=bbbbbbbb:

Critical pair: aabbbbbbbbbbb=babbbbb.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [18] bbbbbbabbbb=abbbbbbb with [24] bbabbbbb=bbbbbbbb:

Critical pair: bbbbbbbbbbbb=abbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32], [35], [36], [37].

Overlap of [24] bbabbbbb=bbbbbbbb with [2] baba=abbb:

Critical pair: bbabbbbabbb=bbbbbbbbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30], [31].

Overlap of [24] bbabbbbb=bbbbbbbb with [6] abbbbbbaa=babbab:

Critical pair: bbbabbab=bbbbbbbbbaa.

Flip LHS and RHS.

Referenced by [30], [33], [35], [41].

Overlap of [24] bbabbbbb=bbbbbbbb with [7] babbbbaa=abbabbbb:

Critical pair: bbabbbbabbabbbb=bbbbbbbbabbbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [33], [39].

Overlap of [24] bbabbbbb=bbbbbbbb with [18] bbbbbbabbbb=abbbbbbb:

Critical pair: bbaabbbbbbb=bbbbbbbbbabbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [32], [33], [34], [35], [36], [37].

Overlap of [4] baabbb=abbbba with [26] babbbbb=bbbbbbbbbb:

Critical pair: baabbbbbbbbbbbb=abbbbaabbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [33], [37], [40].

Overlap of [26] babbbbb=bbbbbbbbbb with [4] baabbb=abbbba:

Critical pair: babbbbabbbba=bbbbbbbbbbaabbb.

Reduce LHS:

Reduce RHS:

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

Overlap of [26] babbbbb=bbbbbbbbbb with [6] abbbbbbaa=babbab:

Critical pair: bbabbab=bbbbbbbbbbbaa.

Reduce RHS:

Referenced by [38], [41], [43].

Overlap of [26] babbbbb=bbbbbbbbbb with [8] bbbaabbaa=aabbab:

Critical pair: babbbbaabbab=bbbbbbbbbbbbaabbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [36].

Simplify [11] baabaabbab=abbbabbbabbaa.

Reduce RHS:

Referenced by [44].

Overlap of [14] aabbbbbabbbb=babbbb with [32] bbbbabbbb=bbbbbbbbb:

Critical pair: aabbbbbbbbbb=babbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [46], [54].

Simplify [17] aabbbbbbabbab=bbabbab.

Reduce RHS:

Referenced by [39].

Overlap of [38] aabbbbbbabbab=bbbbbbbbbb with [30] bbbbabbab=bbbbabbbb:

Critical pair: aabbbbbbabbbb=bbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [40], [41], [42], [43], [44], [45], [46], [47], [48], [50], [51], [52], [53], [54].

Overlap of [18] bbbbbbabbbb=abbbbbbb with [32] bbbbabbbb=bbbbbbbbb:

Critical pair: bbbbbbbbbbb=abbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [46], [47], [49], [51], [53].

Simplify [29] bbbbbbbbbaa=bbbabbab.

Reduce RHS:

Referenced by [42].

Overlap of [41] bbbbbbbbbaa=bbbbbbbb with [33] bbbbbbbba=bbbbbbbbb:

Critical pair: bbbbbbbbbba=bbbbbbbb.

Reduce LHS:

Defines rule #6.

Referenced by [45], [48], [50], [52].

Simplify [34] bbabbab=bbbbbbbbbb.

Reduce RHS:

Defines rule #11.

Simplify [36] baabaabbab=bbbbbbbbbb.

Reduce RHS:

Defines rule #23.

Referenced by [45].

Overlap of [44] baabaabbab=bbbbbbb with [3] abbbaa=bab:

Critical pair: baabaabbbab=bbbbbbbbbaa.

Reduce LHS:

Reduce RHS:

Defines rule #12.

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

Overlap of [4] baabbb=abbbba with [45] bbbbbaab=bbbbbbbb:

Critical pair: baabbbbbbbb=abbbbabbaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [53].

Overlap of [6] abbbbbbaa=babbab with [45] bbbbbaab=bbbbbbbb:

Critical pair: abbbbbbbbb=babbabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [49], [50].

Overlap of [45] bbbbbaab=bbbbbbbb with [8] bbbaabbaa=aabbab:

Critical pair: bbaabbab=bbbbbbbbbaa.

Reduce RHS:

Defines rule #17.

Overlap of [2] baba=abbb with [47] babbabb=bbbbbbb:

Critical pair: babbbbbbb=abbbbbabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [47] babbabb=bbbbbbb with [3] abbbaa=bab:

Critical pair: babbbab=bbbbbbbbaa.

Reduce RHS:

Defines rule #10.

Referenced by [54].

Overlap of [1] aaa=1 with [49] abbbbbabb=bbbbbbbbb:

Critical pair: aabbbbbbbbb=bbbbbabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [52].

Overlap of [51] bbbbbabb=bbbbbbbb with [3] abbbaa=bab:

Critical pair: bbbbbbab=bbbbbbbbbaa.

Reduce RHS:

Defines rule #5.

Overlap of [1] aaa=1 with [46] abbbbabbaab=bbbbbbbb:

Critical pair: aabbbbbbbb=bbbbabbaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [19] aabaabbabbb=bbbbaaba with [50] babbbab=bbbbbbb:

Critical pair: aabaabbbbbbbb=bbbbaabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.