Certificate for #7544 ⟨a, b | aaa=1, babbbb=a⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #3.

Referenced by [4], [5], [10], [11], [12], [14], [15], [17], [18], [19], [23], [24], [26], [28], [29], [30], [31], [33].

Axiom: babbbb=a.

Referenced by [3], [6], [7], [8], [15], [16], [23], [25], [26], [28], [29], [30], [32].

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

Critical pair: babbba=aabbbb.

Flip LHS and RHS.

Referenced by [4], [9].

Overlap of [1] aaa=1 with [3] aabbbb=babbba:

Critical pair: ababbba=bbbb.

Referenced by [5], [12].

Overlap of [4] ababbba=bbbb with [1] aaa=1:

Critical pair: ababbb=bbbbaa.

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

Overlap of [5] ababbb=bbbbaa with [2] babbbb=a:

Critical pair: aa=bbbbaab.

Flip LHS and RHS.

Referenced by [7], [8], [9], [12], [14], [22].

Overlap of [2] babbbb=a with [6] bbbbaab=aa:

Critical pair: babaa=abaab.

Flip LHS and RHS.

Referenced by [10], [17], [24], [30].

Overlap of [2] babbbb=a with [6] bbbbaab=aa:

Critical pair: babbaa=abbaab.

Flip LHS and RHS.

Referenced by [14], [15], [18], [19], [23], [26], [28].

Overlap of [6] bbbbaab=aa with [3] aabbbb=babbba:

Critical pair: bbbbbabbba=aabbb.

Flip LHS and RHS.

Referenced by [22].

Overlap of [1] aaa=1 with [7] abaab=babaa:

Critical pair: aababaa=baab.

Referenced by [11].

Overlap of [10] aababaa=baab with [1] aaa=1:

Critical pair: aabab=baaba.

Referenced by [12].

Overlap of [4] ababbba=bbbb with [11] aabab=baaba:

Critical pair: ababbbbaaba=bbbbabab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [21].

Overlap of [12] bbbbabab=aba with [5] ababbb=bbbbaa:

Critical pair: bbbbbbbbaa=ababb.

Flip LHS and RHS.

Referenced by [21].

Overlap of [8] abbaab=babbaa with [6] bbbbaab=aa:

Critical pair: abbaaaa=babbaabbbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [8] abbaab=babbaa with [14] bbbbabbab=abba:

Critical pair: abbaaabba=babbaabbbabbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [17], [18], [25], [26], [28], [29], [30], [32].

Overlap of [14] bbbbabbab=abba with [2] babbbb=a:

Critical pair: bbbbaba=abbabbb.

Flip LHS and RHS.

Referenced by [20].

Overlap of [7] abaab=babaa with [15] bbbaab=abbbba:

Critical pair: abaaabbbba=babaabbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [8] abbaab=babbaa with [15] bbbaab=abbbba:

Critical pair: abbaaabbbba=babbaabbaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [8] abbaab=babbaa with [17] bbbabab=abbbbba:

Critical pair: abbaaabbbbba=babbaabbabab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [14] bbbbabbab=abba with [16] abbabbb=bbbbaba:

Critical pair: bbbbbbbbaba=abbabb.

Flip LHS and RHS.

Referenced by [25], [26].

Overlap of [12] bbbbabab=aba with [13] ababb=bbbbbbbbaa:

Critical pair: bbbbbbbbbbbbaa=abab.

Flip LHS and RHS.

Referenced by [24], [25].

Overlap of [6] bbbbaab=aa with [9] aabbb=bbbbbabbba:

Critical pair: bbbbbbbbbabbba=aabb.

Flip LHS and RHS.

Referenced by [27].

Overlap of [8] abbaab=babbaa with [18] bbbabbab=abbbbbba:

Critical pair: abbaaabbbbbba=babbaabbabbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [23] bbaab=abbbbbbbba with [7] abaab=babaa:

Critical pair: bbababaa=abbbbbbbbaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [20] abbabb=bbbbbbbbaba with [2] babbbb=a:

Critical pair: aba=bbbbbbbbababb.

Reduce RHS:

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

Overlap of [20] abbabb=bbbbbbbbaba with [15] bbbaab=abbbba:

Critical pair: abbaabbbba=bbbbbbbbababaab.

Reduce LHS:

Reduce RHS:

Referenced by [27], [32].

Simplify [22] aabb=bbbbbbbbbabbba.

Reduce RHS:

Referenced by [28], [29].

Overlap of [27] aabb=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbaa with [8] abbaab=babbaa:

Critical pair: ababbaa=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [27] aabb=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbaa with [15] bbbaab=abbbba:

Critical pair: aaabbbba=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbaabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [7] abaab=babaa with [25] aba=bbbbbbbbbbbbbbbbaa:

Critical pair: ababbbbbbbbbbbbbbbbaa=babaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [25] aba=bbbbbbbbbbbbbbbbaa with [1] aaa=1:

Critical pair: ab=bbbbbbbbbbbbbbbbaaaa.

Reduce RHS:

Defines rule #2.

Overlap of [25] aba=bbbbbbbbbbbbbbbbaa with [2] babbbb=a:

Critical pair: aa=bbbbbbbbbbbbbbbbaabbbb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [32] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbaa=aa with [1] aaa=1:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=aaa.

Reduce RHS:

Defines rule #1.