Certificate for #8067 ⟨a, b | aaa=1, abba=bbb⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #10.

Referenced by [3], [4], [18], [22].

Axiom: abba=bbb.

Defines rule #5.

Referenced by [3], [4], [5], [6], [15], [22], [25].

Overlap of [1] aaa=1 with [2] abba=bbb:

Critical pair: aabbb=bba.

Referenced by [6], [7], [8], [9], [10], [12], [18], [21], [22], [23], [25], [26], [27].

Overlap of [2] abba=bbb with [1] aaa=1:

Critical pair: abb=bbbaa.

Flip LHS and RHS.

Referenced by [7], [11], [15], [16], [18], [20], [21], [25].

Overlap of [2] abba=bbb with [2] abba=bbb:

Critical pair: abbbbb=bbbbba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [8], [13], [14], [17], [19], [20], [21], [22].

Overlap of [2] abba=bbb with [3] aabbb=bba:

Critical pair: abbbba=bbbabbb.

Defines rule #6.

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

Overlap of [3] aabbb=bba with [4] bbbaa=abb:

Critical pair: aababb=bbabaa.

Flip LHS and RHS.

Referenced by [9].

Overlap of [3] aabbb=bba with [5] bbbbba=abbbbb:

Critical pair: aababbbbb=bbabbba.

Referenced by [17], [21], [24].

Overlap of [3] aabbb=bba with [7] bbabaa=aababb:

Critical pair: aabaababb=bbaabaa.

Referenced by [15], [16].

Overlap of [3] aabbb=bba with [6] abbbba=bbbabbb:

Critical pair: abbbabbb=bbaba.

Flip LHS and RHS.

Defines rule #8.

Referenced by [12], [13], [14], [15], [17], [19], [20].

Overlap of [6] abbbba=bbbabbb with [4] bbbaa=abb:

Critical pair: ababb=bbbabbba.

Flip LHS and RHS.

Defines rule #9.

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

Overlap of [3] aabbb=bba with [10] bbaba=abbbabbb:

Critical pair: aababbbabbb=bbaaba.

Referenced by [17].

Overlap of [6] abbbba=bbbabbb with [11] bbbabbba=ababb:

Critical pair: abababb=bbbabbbbbba.

Reduce RHS:

Defines rule #12.

Referenced by [20], [22].

Overlap of [11] bbbabbba=ababb with [10] bbaba=abbbabbb:

Critical pair: bbbababbbabbb=ababbba.

Reduce LHS:

Referenced by [19], [20].

Overlap of [2] abba=bbb with [9] aabaababb=bbaabaa:

Critical pair: abbbbaabaa=bbbabaababb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [9] aabaababb=bbaabaa with [4] bbbaa=abb:

Critical pair: aabaabaabb=bbaabaabaa.

Flip LHS and RHS.

Referenced by [18], [22].

Overlap of [12] aababbbabbb=bbaaba with [6] abbbba=bbbabbb:

Critical pair: aababbbbbbabbb=bbaababa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [4] bbbaa=abb with [16] bbaabaabaa=aabaabaabb:

Critical pair: baabaabaabb=abbbaabaa.

Reduce RHS:

Referenced by [25].

Overlap of [10] bbaba=abbbabbb with [14] bababbbabbbbbbbbbbb=ababbba:

Critical pair: bababbba=abbbabbbbbbabbbbbbbbbbb.

Reduce RHS:

Defines rule #13.

Overlap of [14] bababbbabbbbbbbbbbb=ababbba with [5] bbbbba=abbbbb:

Critical pair: bababbbabbbbbbabbbbb=ababbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [17] bbaababa=ababbbabbbbbbbbbbbbbb with [8] aababbbbb=bbabbba:

Critical pair: bbaababbbabbba=ababbbabbbbbbbbbbbbbbababbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [27].

Overlap of [17] bbaababa=ababbbabbbbbbbbbbbbbb with [15] baababbbabb=abaabb:

Critical pair: bbaabaabaabb=ababbbabbbbbbbbbbbbbbababbbabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [23], [24].

Overlap of [3] aabbb=bba with [22] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bbb:

Critical pair: aabbb=bbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [27], [28].

Overlap of [8] aababbbbb=bbabbba with [22] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bbb:

Critical pair: aababbb=bbabbbabbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Referenced by [28].

Overlap of [18] baabaabaabb=bb with [20] abaabb=abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbb:

Critical pair: baabaabbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bb.

Reduce LHS:

Defines rule #1.

Referenced by [26], [28].

Overlap of [3] aabbb=bba with [25] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bb:

Critical pair: aabb=bbabbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #4.

Referenced by [27].

Overlap of [3] aabbb=bba with [23] bbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bba:

Critical pair: aabbba=bbaabbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Defines rule #7.

Overlap of [24] aababbb=bbabbbabbbbbbbbbbbbbbbbbbbbbbbbbbbb with [25] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=bb:

Critical pair: aababb=bbabbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #11.