Certificate for #19836 ⟨a, b | aaa=a, babb=aba⟩

Completion settings:

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

Axiom: aaa=a.

Defines rule #6.

Referenced by [3], [4], [41].

Axiom: babb=aba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4], [5], [6], [7], [9], [10], [11], [17], [19], [20], [21], [22], [23], [24], [25], [26], [27], [28], [29], [30], [31], [32], [35], [36], [37], [38], [40], [41].

Overlap of [1] aaa=a with [2] aba=babb:

Critical pair: aababb=aba.

Reduce LHS:

Reduce RHS:

Defines rule #1.

Referenced by [11], [12], [21], [22], [25], [27], [28], [29], [31], [32].

Overlap of [2] aba=babb with [1] aaa=a:

Critical pair: aba=babbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [6], [7], [13].

Overlap of [2] aba=babb with [2] aba=babb:

Critical pair: abbabb=babbba.

Defines rule #3.

Referenced by [8], [11], [18], [20], [21], [22], [23], [25], [26], [27], [28], [29], [31], [32], [37], [38], [40], [41].

Overlap of [2] aba=babb with [4] babbaa=babb:

Critical pair: ababb=babbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [9], [14].

Overlap of [4] babbaa=babb with [2] aba=babb:

Critical pair: babbababb=babbba.

Reduce LHS:

Defines rule #4.

Referenced by [15], [19], [22], [24], [26], [28], [30], [32], [35], [36], [38], [40].

Overlap of [5] abbabb=babbba with [5] abbabb=babbba:

Critical pair: abbbabbba=babbbaabb.

Flip LHS and RHS.

Defines rule #12.

Referenced by [10], [11], [16], [19], [20], [21], [24], [25], [26], [27], [28], [30], [31], [32], [35], [36], [38], [40].

Overlap of [6] babbbbaa=babbbb with [2] aba=babb:

Critical pair: babbbbababb=babbbbba.

Reduce LHS:

Defines rule #5.

Referenced by [12], [13], [14], [15], [16], [19], [20], [21], [25], [28], [32], [37], [41].

Overlap of [2] aba=babb with [8] babbbaabb=abbbabbba:

Critical pair: aabbbabbba=babbbbbaabb.

Defines rule #16.

Referenced by [17], [21], [27], [31], [36].

Overlap of [3] babbbbbb=babb with [8] babbbaabb=abbbabbba:

Critical pair: babbbbbabbbabbba=babbabbbaabb.

Reduce RHS:

Referenced by [16], [19], [20], [21], [27].

Overlap of [9] babbbbbabbbb=babbbbba with [3] babbbbbb=babb:

Critical pair: babbbbbabbbbabb=babbbbbaabbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [27], [28].

Overlap of [9] babbbbbabbbb=babbbbba with [4] babbaa=babb:

Critical pair: babbbbbabbbbabb=babbbbbaabbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Overlap of [9] babbbbbabbbb=babbbbba with [6] babbbbaa=babbbb:

Critical pair: babbbbbabbbbabbbb=babbbbbaabbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Overlap of [9] babbbbbabbbb=babbbbba with [7] babbbabbbb=babbba:

Critical pair: babbbbbabbbbabbba=babbbbbaabbbabbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [9] babbbbbabbbb=babbbbba with [8] babbbaabb=abbbabbba:

Critical pair: babbbbbabbbabbbabbba=babbbbbaabbbaabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Referenced by [18].

Overlap of [10] aabbbabbba=babbbbbaabb with [2] aba=babb:

Critical pair: aabbbabbbbabb=babbbbbaabbba.

Referenced by [18], [21], [28], [32].

Overlap of [17] aabbbabbbbabb=babbbbbaabbba with [5] abbabb=babbba:

Critical pair: aabbbabbbbbabbba=babbbbbaabbbaabb.

Reduce RHS:

Referenced by [33].

Overlap of [11] babbbbbabbbabbba=bbabbbbbabbba with [2] aba=babb:

Critical pair: babbbbbabbbabbbbabb=bbabbbbbabbbaba.

Reduce LHS:

Reduce RHS:

Referenced by [20], [22], [23], [24], [25], [26], [28].

Overlap of [11] babbbbbabbbabbba=bbabbbbbabbba with [8] babbbaabb=abbbabbba:

Critical pair: babbbbbabbbabbabbbabbba=bbabbbbbabbbabbbaabb.

Reduce LHS:

Reduce RHS:

Referenced by [32].

Overlap of [17] aabbbabbbbabb=babbbbbaabbba with [11] babbbbbabbbabbba=bbabbbbbabbba:

Critical pair: aabbbabbbbbabbbbbabbba=babbbbbaabbbabbbabbbabbba.

Reduce LHS:

Reduce RHS:

Referenced by [32].

Overlap of [3] babbbbbb=babb with [19] babbbbabbbabbba=bbabbbbbaabb:

Critical pair: babbbbbbbabbbbbaabb=babbabbbbabbbabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [26], [27], [28].

Overlap of [5] abbabb=babbba with [19] babbbbabbbabbba=bbabbbbbaabb:

Critical pair: abbbabbbbbaabb=babbbabbabbbabbba.

Reduce RHS:

Referenced by [34].

Overlap of [19] babbbbabbbabbba=bbabbbbbaabb with [2] aba=babb:

Critical pair: babbbbabbbabbbbabb=bbabbbbbaabbba.

Reduce LHS:

Referenced by [31], [32], [36], [37], [38], [39].

Overlap of [19] babbbbabbbabbba=bbabbbbbaabb with [8] babbbaabb=abbbabbba:

Critical pair: babbbbabbabbbabbba=bbabbbbbaabbabb.

Reduce LHS:

Reduce RHS:

Defines rule #20.

Referenced by [26], [27], [28].

Overlap of [19] babbbbabbbabbba=bbabbbbbaabb with [8] babbbaabb=abbbabbba:

Critical pair: babbbbabbbabbabbbabbba=bbabbbbbaabbbbbaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [25] babbbbbaabbbbba=bbbabbbabbba with [10] aabbbabbba=babbbbbaabb:

Critical pair: babbbbbaabbbbbbabbbbbaabb=bbbabbbabbbaabbbabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [25] babbbbbaabbbbba=bbbabbbabbba with [17] aabbbabbbbabb=babbbbbaabbba:

Critical pair: babbbbbaabbbbbbabbbbbaabbba=bbbabbbabbbaabbbabbbbabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [29], [39], [41].

Overlap of [28] bbbbbabbbbbaabb=babbbbbaabb with [5] abbabb=babbba:

Critical pair: bbbbbabbbbbababbba=babbbbbaabbabb.

Reduce LHS:

Reduce RHS:

Referenced by [30].

Overlap of [29] bbbbbbabbbabbba=bbabbbabbba with [2] aba=babb:

Critical pair: bbbbbbabbbabbbbabb=bbabbbabbbaba.

Reduce LHS:

Reduce RHS:

Referenced by [31], [32].

Overlap of [5] abbabb=babbba with [30] bbbbbabbbabbba=babbbabbba:

Critical pair: abbababbbabbba=babbbabbbabbbabbba.

Reduce LHS:

Reduce RHS:

Defines rule #18.

Referenced by [33].

Overlap of [17] aabbbabbbbabb=babbbbbaabbba with [30] bbbbbabbbabbba=babbbabbba:

Critical pair: aabbbabbbbababbbabbba=babbbbbaabbbabbbabbbabbba.

Reduce LHS:

Reduce RHS:

Defines rule #9.

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

Overlap of [18] aabbbabbbbbabbba=bbbabbbbbabbba with [31] abbbabbbbbabbba=bbbbabbbbabbbbba:

Critical pair: abbbbabbbbabbbbba=bbbabbbbbabbba.

Defines rule #21.

Referenced by [34].

Simplify [23] abbbabbbbbaabb=babbbbabbbbabbbbba.

Reduce RHS:

Defines rule #22.

Referenced by [37], [41].

Overlap of [32] bbbbabbbabbba=abbbabbba with [2] aba=babb:

Critical pair: bbbbabbbabbbbabb=abbbabbbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [36].

Overlap of [35] abbbabbbbabb=bbbabbbabbba with [32] bbbbabbbabbba=abbbabbba:

Critical pair: abbbaabbbabbba=bbbabbbabbbababbba.

Reduce LHS:

Reduce RHS:

Defines rule #23.

Overlap of [5] abbabb=babbba with [24] babbbabbbabbba=bbabbbbbaabbba:

Critical pair: abbbabbbbbaabbba=babbbababbbabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [24] babbbabbbabbba=bbabbbbbaabbba with [2] aba=babb:

Critical pair: babbbabbbabbbbabb=bbabbbbbaabbbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [32] bbbbabbbabbba=abbbabbba with [24] babbbabbbabbba=bbabbbbbaabbba:

Critical pair: bbbbbabbbbbaabbba=abbbabbbabbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [40].

Overlap of [39] abbbabbbabbba=babbbbbaabbba with [2] aba=babb:

Critical pair: abbbabbbabbbbabb=babbbbbaabbbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [34] abbbabbbbbaabb=bbbbabbbbbabbba with [32] bbbbabbbabbba=abbbabbba:

Critical pair: abbbabbbbbaaabbbabbba=bbbbabbbbbabbbabbabbbabbba.

Reduce LHS:

Reduce RHS:

Defines rule #19.