Certificate for #14363 ⟨a, b | aaaa=a, babbb=a⟩

Completion settings:

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

Axiom: aaaa=a.

Defines rule #5.

Referenced by [4], [5], [8], [12], [17], [24], [25], [27], [28], [29], [31], [32].

Axiom: babbb=a.

Referenced by [3], [6], [7], [9], [10], [11], [12], [13], [14], [15], [16], [18], [19], [23], [25], [26], [29], [30], [31], [33].

Overlap of [2] babbb=a with [2] babbb=a:

Critical pair: babba=aabbb.

Flip LHS and RHS.

Referenced by [4], [10], [11], [12], [16], [18], [23], [24], [29], [31].

Overlap of [1] aaaa=a with [3] aabbb=babba:

Critical pair: aababba=abbb.

Referenced by [5], [6], [9].

Overlap of [4] aababba=abbb with [1] aaaa=a:

Critical pair: aababba=abbbaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [4] aababba=abbb with [2] babbb=a:

Critical pair: aababa=abbbbbb.

Referenced by [7], [10].

Overlap of [6] aababa=abbbbbb with [2] babbb=a:

Critical pair: aabaa=abbbbbbbbb.

Referenced by [8], [9], [10], [11], [12].

Overlap of [7] aabaa=abbbbbbbbb with [1] aaaa=a:

Critical pair: aaba=abbbbbbbbbaa.

Referenced by [12], [22], [24], [29], [30], [31].

Overlap of [7] aabaa=abbbbbbbbb with [4] aababba=abbb:

Critical pair: aababbb=abbbbbbbbbbabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [31].

Overlap of [7] aabaa=abbbbbbbbb with [6] aababa=abbbbbb:

Critical pair: aababbbbbb=abbbbbbbbbbaba.

Reduce LHS:

Referenced by [15], [16], [20].

Overlap of [7] aabaa=abbbbbbbbb with [7] aabaa=abbbbbbbbb:

Critical pair: aababbbbbbbbb=abbbbbbbbbbaa.

Reduce LHS:

Referenced by [16], [23], [25], [27].

Overlap of [7] aabaa=abbbbbbbbb with [8] aaba=abbbbbbbbbaa:

Critical pair: aabaabbbbbbbbbaa=abbbbbbbbbaba.

Reduce LHS:

Referenced by [19], [21].

Overlap of [2] babbb=a with [9] abbbbbbbbbbabba=aaa:

Critical pair: baaa=abbbbbbbabba.

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] babbb=a with [13] abbbbbbbabba=baaa:

Critical pair: bbaaa=abbbbabba.

Flip LHS and RHS.

Referenced by [15], [16].

Overlap of [2] babbb=a with [14] abbbbabba=bbaaa:

Critical pair: bbbaaa=ababba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [3] aabbb=babba with [14] abbbbabba=bbaaa:

Critical pair: abbaaa=babbababba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [16] bbbabbabaa=abbaaa with [1] aaaa=a:

Critical pair: bbbabbaba=abbaaaaa.

Reduce RHS:

Referenced by [18].

Overlap of [17] bbbabbaba=abbaa with [2] babbb=a:

Critical pair: bbbabbaa=abbaabbb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [2] babbb=a with [18] abbbabba=bbbabbaa:

Critical pair: bbbbabbaa=aabba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [21].

Simplify [10] ababba=abbbbbbbbbbaba.

Reduce RHS:

Referenced by [22], [23], [24], [25].

Simplify [12] aabba=abbbbbbbbbaba.

Reduce RHS:

Referenced by [22], [25], [30], [31].

Overlap of [8] aaba=abbbbbbbbbaa with [20] ababba=bbbaaa:

Critical pair: abbbaaa=abbbbbbbbbaabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30], [32].

Overlap of [20] ababba=bbbaaa with [2] babbb=a:

Critical pair: ababa=bbbaaabbb.

Reduce LHS:

Reduce RHS:

Referenced by [25], [27].

Overlap of [20] ababba=bbbaaa with [8] aaba=abbbbbbbbbaa:

Critical pair: ababbabbbbbbbbbaa=bbbaaaaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [11] ababa=abbbbbbbbbbaa with [20] ababba=bbbaaa:

Critical pair: abbbbaaa=abbbbbbbbbbaabba.

Reduce RHS:

Referenced by [26].

Overlap of [2] babbb=a with [25] abbbbaaa=bbbbbbbba:

Critical pair: bbbbbbbbba=abaaa.

Flip LHS and RHS.

Referenced by [27], [28], [29], [30].

Overlap of [11] ababa=abbbbbbbbbbaa with [26] abaaa=bbbbbbbbba:

Critical pair: abbbbbbbbbba=abbbbbbbbbbaaaa.

Reduce RHS:

Referenced by [31].

Overlap of [26] abaaa=bbbbbbbbba with [1] aaaa=a:

Critical pair: aba=bbbbbbbbbaa.

Defines rule #3.

Referenced by [31].

Overlap of [26] abaaa=bbbbbbbbba with [8] aaba=abbbbbbbbbaa:

Critical pair: abaabbbbbbbbbaa=bbbbbbbbbaba.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [30], [31], [32].

Overlap of [26] abaaa=bbbbbbbbba with [21] aabba=bbbbabbaa:

Critical pair: ababbbbabbaa=bbbbbbbbbabba.

Reduce LHS:

Reduce RHS:

Referenced by [32].

Overlap of [9] abbbbbbbbbbabba=aaa with [28] aba=bbbbbbbbbaa:

Critical pair: abbbbbbbbbbabbbbbbbbbbbaa=aaaba.

Reduce LHS:

Reduce RHS:

Referenced by [32], [33].

Simplify [22] abbbbbbbbbbbbbabbaa=abbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [31] bbbbbbbbbbbbbbbbbbbbbbbbbbbbba=ba with [2] babbb=a:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbba=babbb.

Reduce RHS:

Defines rule #1.