Certificate for #10757 ⟨a, b | aaab=bba, abab=1⟩

Completion settings:

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

Axiom: aaab=bba.

Referenced by [3], [6], [14].

Axiom: abab=1.

Referenced by [3], [4], [8], [10], [16], [23].

Overlap of [1] aaab=bba with [2] abab=1:

Critical pair: aa=bbaab.

Flip LHS and RHS.

Referenced by [4], [5], [7], [8], [9], [12], [15].

Overlap of [2] abab=1 with [3] bbaab=aa:

Critical pair: abaaa=baab.

Referenced by [6].

Overlap of [3] bbaab=aa with [3] bbaab=aa:

Critical pair: bbaaaa=aabaab.

Referenced by [18].

Overlap of [4] abaaa=baab with [1] aaab=bba:

Critical pair: abbba=baabb.

Flip LHS and RHS.

Referenced by [7], [17], [22], [23].

Overlap of [3] bbaab=aa with [6] baabb=abbba:

Critical pair: babbba=aab.

Referenced by [8], [9], [11], [13], [24].

Overlap of [7] babbba=aab with [3] bbaab=aa:

Critical pair: babaa=aabab.

Reduce RHS:

Referenced by [10].

Overlap of [7] babbba=aab with [7] babbba=aab:

Critical pair: babbaab=aabbbba.

Reduce LHS:

Referenced by [20].

Overlap of [8] babaa=a with [2] abab=1:

Critical pair: baba=abab.

Reduce RHS:

Referenced by [11], [19], [22], [27], [28], [30], [31].

Overlap of [7] babbba=aab with [10] baba=1:

Critical pair: babb=aabba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [12], [13], [26], [27].

Overlap of [3] bbaab=aa with [11] aabba=babb:

Critical pair: bbbabb=aaba.

Flip LHS and RHS.

Referenced by [13], [14], [15], [16], [17], [18], [23], [26].

Overlap of [11] aabba=babb with [7] babbba=aab:

Critical pair: aabaab=babbbbba.

Reduce LHS:

Referenced by [17], [18].

Overlap of [1] aaab=bba with [12] aaba=bbbabb:

Critical pair: abbbabb=bbaa.

Flip LHS and RHS.

Referenced by [19].

Overlap of [3] bbaab=aa with [12] aaba=bbbabb:

Critical pair: bbbbbabb=aaa.

Flip LHS and RHS.

Referenced by [17], [20], [22], [32].

Overlap of [12] aaba=bbbabb with [2] abab=1:

Critical pair: a=bbbabbb.

Flip LHS and RHS.

Referenced by [17], [22], [23], [24], [25], [29], [30].

Overlap of [12] aaba=bbbabb with [6] baabb=abbba:

Critical pair: aaabbba=bbbabbabb.

Reduce LHS:

Reduce RHS:

Referenced by [19], [21].

Simplify [5] bbaaaa=aabaab.

Reduce RHS:

Referenced by [19].

Overlap of [18] bbaaaa=babbbbba with [14] bbaa=abbbabb:

Critical pair: abbbabbaa=babbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [9] baaa=aabbbba with [15] aaa=bbbbbabb:

Critical pair: bbbbbbabb=aabbbba.

Flip LHS and RHS.

Referenced by [27].

Simplify [17] bbabba=babbbbbab.

Reduce RHS:

Referenced by [23], [25], [26].

Overlap of [6] baabb=abbba with [16] bbbabbb=a:

Critical pair: baaa=abbbababbb.

Reduce LHS:

Reduce RHS:

Referenced by [27].

Overlap of [6] baabb=abbba with [16] bbbabbb=a:

Critical pair: baaba=abbbabbabbb.

Reduce LHS:

Reduce RHS:

Referenced by [32].

Overlap of [7] babbba=aab with [16] bbbabbb=a:

Critical pair: baa=aabbbb.

Defines rule #4.

Referenced by [26], [27].

Overlap of [16] bbbabbb=a with [16] bbbabbb=a:

Critical pair: bbbabba=abbabbb.

Reduce LHS:

Referenced by [26].

Overlap of [11] aabba=babb with [24] baa=aabbbb:

Critical pair: aabaabbbb=babba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [24] baa=aabbbb with [11] aabba=babb:

Critical pair: bababb=aabbbbabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [27] abbbbbbba=bb with [10] baba=1:

Critical pair: abbbbbb=bbba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [29], [30].

Overlap of [16] bbbabbb=a with [28] bbba=abbbbbb:

Critical pair: abbbbbbbbb=a.

Referenced by [31].

Overlap of [16] bbbabbb=a with [28] bbba=abbbbbb:

Critical pair: bbbababbbbbb=aba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [10] baba=1 with [29] abbbbbbbbb=a:

Critical pair: baba=bbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Simplify [15] aaa=bbbbbabb.

Reduce RHS:

Defines rule #6.