Certificate for #27125 ⟨a, b | aa=1, ababbba=bb⟩

Completion settings:

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

Axiom: aa=1.

Defines rule #4.

Referenced by [3], [4], [5], [10], [11], [14], [16], [17], [23].

Axiom: ababbba=bb.

Referenced by [3], [4], [7], [16].

Overlap of [1] aa=1 with [2] ababbba=bb:

Critical pair: abb=babbba.

Flip LHS and RHS.

Referenced by [7], [8], [9], [10], [12], [16], [19], [26].

Overlap of [2] ababbba=bb with [1] aa=1:

Critical pair: ababbb=bba.

Referenced by [5], [6], [9], [10], [18], [20].

Overlap of [1] aa=1 with [4] ababbb=bba:

Critical pair: abba=babbb.

Defines rule #6.

Referenced by [6], [7], [8], [9], [13].

Overlap of [5] abba=babbb with [4] ababbb=bba:

Critical pair: abbbba=babbbbabbb.

Flip LHS and RHS.

Referenced by [11], [17].

Overlap of [2] ababbba=bb with [3] babbba=abb:

Critical pair: ababbabb=bbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9], [10], [11], [12], [13], [15], [17], [19].

Overlap of [5] abba=babbb with [3] babbba=abb:

Critical pair: ababb=babbbbbba.

Reduce RHS:

Referenced by [20], [21].

Overlap of [4] ababbb=bba with [7] bbbbba=babbbbbbbb:

Critical pair: ababbabbbbbbbb=bbabbba.

Reduce LHS:

Reduce RHS:

Referenced by [13], [15].

Overlap of [4] ababbb=bba with [7] bbbbba=babbbbbbbb:

Critical pair: ababbbabbbbbbbb=bbabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [7] bbbbba=babbbbbbbb with [1] aa=1:

Critical pair: bbbbb=babbbbbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [14].

Overlap of [7] bbbbba=babbbbbbbb with [3] babbba=abb:

Critical pair: bbbbabb=babbbbbbbbbbba.

Reduce RHS:

Referenced by [14], [17], [19], [24].

Overlap of [7] bbbbba=babbbbbbbb with [5] abba=babbb:

Critical pair: bbbbbbabbb=babbbbbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [15], [20].

Simplify [11] abbbbabbbbb=bbbbb.

Reduce LHS:

Referenced by [15].

Overlap of [14] bbbbbbbbbbbbbbbbbbbbb=bbbbb with [7] bbbbba=babbbbbbbb:

Critical pair: bbbbbbbbbbbbbbbbbabbbbbbbb=bbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [17], [19], [20].

Overlap of [2] ababbba=bb with [15] babbbbbbbb=babbbb:

Critical pair: ababbbabbbb=bbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [15] babbbbbbbb=babbbb with [7] bbbbba=babbbbbbbb:

Critical pair: babbbbabbbbbbbb=babbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [4] ababbb=bba with [17] babbbba=bbbbbbbbb:

Critical pair: abbbbbbbbb=bbaba.

Flip LHS and RHS.

Referenced by [25].

Overlap of [17] babbbba=bbbbbbbbb with [3] babbba=abb:

Critical pair: babbbabb=bbbbbbbbbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [24], [25].

Overlap of [4] ababbb=bba with [8] ababb=bbabbbbbbbbbbb:

Critical pair: bbabbbbbbbbbbbb=bba.

Reduce LHS:

Defines rule #2.

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

Simplify [8] ababb=bbabbbbbbbbbbb.

Reduce RHS:

Defines rule #5.

Simplify [10] bbabbbba=bbbbbbbbbb.

Reduce RHS:

Referenced by [23].

Overlap of [22] bbabbbba=bbbbbb with [20] bbabbbb=bba:

Critical pair: bbaa=bbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [24].

Simplify [12] bbbbabb=abbbbbbbbbbbbbbbbbb.

Reduce RHS:

Referenced by [26], [27].

Simplify [18] bbaba=abbbbbbbbb.

Reduce RHS:

Defines rule #8.

Overlap of [24] bbbbabb=abb with [3] babbba=abb:

Critical pair: bbbabb=abbba.

Flip LHS and RHS.

Defines rule #7.

Overlap of [24] bbbbabb=abb with [20] bbabbbb=bba:

Critical pair: bbbba=abbbb.

Defines rule #3.