Certificate for #7799 ⟨a, b | aaa=1, abbba=bb⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #11.

Referenced by [3], [4], [6], [15], [23].

Axiom: abbba=bb.

Defines rule #6.

Referenced by [3], [4], [5], [7], [13], [22].

Overlap of [1] aaa=1 with [2] abbba=bb:

Critical pair: aabb=bbba.

Defines rule #4.

Referenced by [6], [10], [14], [18], [19], [27].

Overlap of [2] abbba=bb with [1] aaa=1:

Critical pair: abbb=bbaa.

Flip LHS and RHS.

Defines rule #7.

Referenced by [7], [8], [9], [19].

Overlap of [2] abbba=bb with [2] abbba=bb:

Critical pair: abbbbb=bbbbba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [12], [16], [19], [23], [24], [28].

Overlap of [1] aaa=1 with [3] aabb=bbba:

Critical pair: aabbba=abb.

Reduce LHS:

Referenced by [10], [11], [13], [14], [17], [20], [21].

Overlap of [2] abbba=bb with [4] bbaa=abbb:

Critical pair: ababbb=bba.

Referenced by [8], [9], [11], [12], [14], [17], [19], [20], [21], [22], [23], [29].

Overlap of [4] bbaa=abbb with [7] ababbb=bba:

Critical pair: bbabba=abbbbabbb.

Defines rule #9.

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

Overlap of [7] ababbb=bba with [4] bbaa=abbb:

Critical pair: ababbabbb=bbabaa.

Flip LHS and RHS.

Referenced by [19], [21].

Overlap of [6] bbbaba=abb with [3] aabb=bbba:

Critical pair: bbbabbbba=abbabb.

Defines rule #10.

Referenced by [16].

Overlap of [7] ababbb=bba with [6] bbbaba=abb:

Critical pair: abababb=bbababa.

Flip LHS and RHS.

Referenced by [13], [14], [17], [22].

Overlap of [7] ababbb=bba with [5] bbbbba=abbbbb:

Critical pair: ababbabbbbb=bbabbbba.

Referenced by [19].

Overlap of [6] bbbaba=abb with [11] bbababa=abababb:

Critical pair: babababb=abbba.

Reduce RHS:

Referenced by [22].

Overlap of [11] bbababa=abababb with [3] aabb=bbba:

Critical pair: bbababbbba=abababbabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [1] aaa=1 with [14] abababbabb=babb:

Critical pair: aababb=bababbabb.

Flip LHS and RHS.

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

Overlap of [10] bbbabbbba=abbabb with [8] bbabba=abbbbabbb:

Critical pair: bbbabbabbbbabbb=abbabbbba.

Reduce LHS:

Referenced by [25].

Overlap of [15] bababbabb=aababb with [6] bbbaba=abb:

Critical pair: bababbababb=aababbbbaba.

Reduce RHS:

Referenced by [20].

Overlap of [15] bababbabb=aababb with [8] bbabba=abbbbabbb:

Critical pair: babaabbbbabbb=aababba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [9] bbabaa=ababbabbb with [12] ababbabbbbb=bbabbbba:

Critical pair: bbababbabbbba=ababbabbbbabbabbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [20].

Simplify [17] bababbababb=aabababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21], [22], [23].

Overlap of [9] bbabaa=ababbabbb with [20] aabababb=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb:

Critical pair: bbababbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=ababbabbbbababb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [11] bbababa=abababb with [20] aabababb=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb:

Critical pair: bbabababbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=abababbabababb.

Reduce LHS:

Reduce RHS:

Defines rule #1.

Referenced by [27], [28].

Overlap of [20] aabababb=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [15] bababbabb=aababb:

Critical pair: aaaababb=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbabb.

Reduce LHS:

Reduce RHS:

Defines rule #5.

Referenced by [24], [29].

Simplify [18] aababba=babbabbbbabbbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25], [26].

Simplify [16] babbabbbbabbbbbbbbbbb=abbabbbba.

Reduce LHS:

Referenced by [26].

Overlap of [24] babbabbbbabbbbbb=abbabbbbabbbbbbbbbbbbbbbbbbbbbbbbb with [25] abbabbbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=abbabbbba:

Critical pair: babbabbbba=abbabbbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #12.

Overlap of [3] aabb=bbba with [22] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bb:

Critical pair: aabb=bbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [22] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bb with [5] bbbbba=abbbbb:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbabbbbb=bba.

Reduce LHS:

Defines rule #2.

Referenced by [29].

Overlap of [7] ababbb=bba with [28] bbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bba:

Critical pair: ababbbba=bbababbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Defines rule #8.