Certificate for #11604 ⟨a, b | baabb=a, bbbbb=1⟩

Completion settings:

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

Axiom: baabb=a.

Referenced by [3], [10].

Axiom: bbbbb=1.

Defines rule #1.

Referenced by [3], [4], [7], [11], [12], [13], [14], [15], [16], [17], [18], [19], [20], [22], [23], [24].

Overlap of [1] baabb=a with [2] bbbbb=1:

Critical pair: baa=abbb.

Referenced by [4], [5], [9], [13].

Overlap of [2] bbbbb=1 with [3] baa=abbb:

Critical pair: bbbbabbb=aa.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6], [13], [14], [16], [17], [18], [19].

Overlap of [3] baa=abbb with [4] aa=bbbbabbb:

Critical pair: babbbbabbb=abbba.

Referenced by [7], [8].

Overlap of [4] aa=bbbbabbb with [4] aa=bbbbabbb:

Critical pair: abbbbabbb=bbbbabbba.

Flip LHS and RHS.

Referenced by [15], [17], [23].

Overlap of [5] babbbbabbb=abbba with [2] bbbbb=1:

Critical pair: babbbba=abbbabb.

Defines rule #5.

Referenced by [9], [13], [14], [15], [17], [18], [19].

Overlap of [5] babbbbabbb=abbba with [5] babbbbabbb=abbba:

Critical pair: babbbabbba=abbbababbb.

Referenced by [11], [17].

Overlap of [7] babbbba=abbbabb with [3] baa=abbb:

Critical pair: babbbabbb=abbbabba.

Flip LHS and RHS.

Referenced by [10], [11], [14].

Overlap of [1] baabb=a with [9] abbbabba=babbbabbb:

Critical pair: bababbbabbb=ababba.

Referenced by [12], [13].

Overlap of [9] abbbabba=babbbabbb with [9] abbbabba=babbbabbb:

Critical pair: abbbabbbabbbabbb=babbbabbbbbbabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [10] bababbbabbb=ababba with [2] bbbbb=1:

Critical pair: bababbba=ababbabb.

Referenced by [13], [14], [18].

Overlap of [10] bababbbabbb=ababba with [7] babbbba=abbbabb:

Critical pair: bababbbabbabbbabb=ababbaabbbba.

Reduce LHS:

Reduce RHS:

Referenced by [16].

Overlap of [12] bababbba=ababbabb with [9] abbbabba=babbbabbb:

Critical pair: babbabbbabbb=ababbabbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [6] bbbbabbba=abbbbabbb with [7] babbbba=abbbabb:

Critical pair: bbbbabbabbbabb=abbbbabbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [16].

Overlap of [13] bbbabbabbabbbabbbb=abababba with [15] bbabbabbbabbbb=abbbbabba:

Critical pair: bbbaabbbbabba=abababba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [18], [19].

Overlap of [6] bbbbabbba=abbbbabbb with [16] abababba=bbabbabba:

Critical pair: bbbbabbbbbabbabba=abbbbabbbbababba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [16] abababba=bbabbabba with [7] babbbba=abbbabb:

Critical pair: ababababbbabb=bbabbabbabbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [16] abababba=bbabbabba with [16] abababba=bbabbabba:

Critical pair: abababbbbabbabba=bbabbabbabababba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [2] bbbbb=1 with [19] bbaba=bbbbab:

Critical pair: bbbbbbbab=aba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [21].

Overlap of [20] aba=bbab with [20] aba=bbab:

Critical pair: abbbab=bbabba.

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [2] bbbbb=1 with [21] bbabba=abbbab:

Critical pair: bbbabbbab=abba.

Referenced by [24].

Overlap of [2] bbbbb=1 with [21] bbabba=abbbab:

Critical pair: bbbbabbbab=babba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Overlap of [22] bbbabbbab=abba with [2] bbbbb=1:

Critical pair: bbbabbba=abbabbbb.

Defines rule #6.