Certificate for #220 ⟨a, b | aabba=ab⟩

Completion settings:

• Auxiliary generators:
  1. c = bbbabba
• Reduction order:
  • Right-to-left recursive path with deg(b) = deg(c) = 0, b < c; deg(a) = 1

Axiom: aabba=ab.

Defines rule #27.

Referenced by [3], [4], [5], [6], [7], [13], [16], [23], [24], [25], [27], [28], [29].

Axiom: bbbabba=c.

Defines rule #19.

Referenced by [4], [8], [9], [10], [11], [12], [15], [17], [23], [24], [27], [28], [29].

Overlap of [1] aabba=ab with [1] aabba=ab:

Critical pair: aabbab=ababba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Referenced by [7], [8], [9], [14], [18].

Overlap of [2] bbbabba=c with [1] aabba=ab:

Critical pair: bbbabbab=cabba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [5], [10], [19], [26].

Overlap of [4] cabba=cb with [1] aabba=ab:

Critical pair: cabbab=cbabba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [6], [9], [11], [20].

Overlap of [5] cbabba=cbb with [1] aabba=ab:

Critical pair: cbabbab=cbbabba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [12], [15], [21].

Overlap of [1] aabba=ab with [3] ababba=abb:

Critical pair: aabbabb=abbabba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [16], [17], [18], [19], [20], [21], [22].

Overlap of [3] ababba=abb with [3] ababba=abb:

Critical pair: ababbabb=abbbabba.

Reduce LHS:

Reduce RHS:

Defines rule #15.

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

Overlap of [5] cbabba=cbb with [3] ababba=abb:

Critical pair: cbabbabb=cbbbabba.

Reduce LHS:

Reduce RHS:

Defines rule #3.

Referenced by [10], [11], [12], [20], [21].

Overlap of [9] cbbbb=cc with [2] bbbabba=c:

Critical pair: cbc=ccabba.

Reduce RHS:

Defines rule #1.

Referenced by [26].

Overlap of [9] cbbbb=cc with [2] bbbabba=c:

Critical pair: cbbc=ccbabba.

Reduce RHS:

Defines rule #2.

Overlap of [9] cbbbb=cc with [2] bbbabba=c:

Critical pair: cbbbc=ccbbabba.

Reduce RHS:

Defines rule #4.

Overlap of [1] aabba=ab with [8] abbbb=ac:

Critical pair: aabbac=abbbbb.

Reduce LHS:

Reduce RHS:

Defines rule #9.

Referenced by [25].

Overlap of [3] ababba=abb with [8] abbbb=ac:

Critical pair: ababbac=abbbbbb.

Reduce LHS:

Reduce RHS:

Defines rule #14.

Overlap of [8] abbbb=ac with [2] bbbabba=c:

Critical pair: abbbc=acbbabba.

Reduce RHS:

Defines rule #16.

Overlap of [1] aabba=ab with [7] abbabba=abbb:

Critical pair: aabbb=abbba.

Defines rule #24.

Referenced by [28].

Overlap of [2] bbbabba=c with [7] abbabba=abbb:

Critical pair: bbbabbb=cbba.

Defines rule #12.

Referenced by [29].

Overlap of [3] ababba=abb with [7] abbabba=abbb:

Critical pair: ababbb=abbbba.

Reduce RHS:

Defines rule #25.

Referenced by [24].

Overlap of [4] cabba=cb with [7] abbabba=abbb:

Critical pair: cabbb=cbbba.

Defines rule #10.

Referenced by [27].

Overlap of [5] cbabba=cbb with [7] abbabba=abbb:

Critical pair: cbabbb=cbbbba.

Reduce RHS:

Defines rule #11.

Referenced by [23].

Overlap of [6] cbbabba=cbbb with [7] abbabba=abbb:

Critical pair: cbbabbb=cbbbbba.

Reduce RHS:

Defines rule #13.

Overlap of [7] abbabba=abbb with [7] abbabba=abbb:

Critical pair: abbabbb=abbbbba.

Reduce RHS:

Defines rule #26.

Overlap of [20] cbabbb=cca with [2] bbbabba=c:

Critical pair: cbac=ccaabba.

Reduce RHS:

Defines rule #6.

Overlap of [18] ababbb=aca with [2] bbbabba=c:

Critical pair: abac=acaabba.

Reduce RHS:

Defines rule #22.

Referenced by [25], [26].

Overlap of [1] aabba=ab with [24] abac=acab:

Critical pair: aabbacab=abbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [4] cabba=cb with [24] abac=acab:

Critical pair: cabbacab=cbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [19] cabbb=cbbba with [2] bbbabba=c:

Critical pair: cac=cbbbaabba.

Reduce RHS:

Defines rule #5.

Overlap of [16] aabbb=abbba with [2] bbbabba=c:

Critical pair: aac=abbbaabba.

Reduce RHS:

Defines rule #21.

Overlap of [17] bbbabbb=cbba with [2] bbbabba=c:

Critical pair: bbbac=cbbaabba.

Reduce RHS:

Defines rule #7.