Certificate for #4292 ⟨a, b | ababaabba=ab⟩

Completion settings:

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

Axiom: ababaabba=ab.

Referenced by [3].

Axiom: baabba=c.

Referenced by [3], [4], [5], [8], [9], [10].

Overlap of [1] ababaabba=ab with [2] baabba=c:

Critical pair: abac=ab.

Defines rule #6.

Referenced by [5], [6], [11], [16], [22], [30], [35].

Overlap of [2] baabba=c with [2] baabba=c:

Critical pair: baabc=cabba.

Flip LHS and RHS.

Defines rule #10.

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

Overlap of [2] baabba=c with [3] abac=ab:

Critical pair: baabbab=cbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [6], [7], [12], [18], [23], [31], [36].

Overlap of [3] abac=ab with [5] cbac=cb:

Critical pair: abacb=abbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [8], [13], [15], [19], [24], [32], [37], [40].

Overlap of [5] cbac=cb with [5] cbac=cb:

Critical pair: cbacb=cbbac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [14], [33].

Overlap of [2] baabba=c with [6] abbac=abb:

Critical pair: baabb=cc.

Defines rule #23.

Referenced by [9], [10], [17], [34].

Overlap of [2] baabba=c with [8] baabb=cc:

Critical pair: cca=c.

Defines rule #1.

Referenced by [11], [12], [13], [14], [20], [25], [29], [33], [38].

Overlap of [2] baabba=c with [8] baabb=cc:

Critical pair: baabcc=cabb.

Defines rule #17.

Referenced by [33].

Overlap of [3] abac=ab with [9] cca=c:

Critical pair: abac=abca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [17], [21], [26], [34], [39].

Overlap of [5] cbac=cb with [9] cca=c:

Critical pair: cbac=cbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [15], [27].

Overlap of [6] abbac=abb with [9] cca=c:

Critical pair: abbac=abbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [28].

Overlap of [7] cbbac=cbb with [9] cca=c:

Critical pair: cbbac=cbbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [6] abbac=abb with [12] cbca=cb:

Critical pair: abbacb=abbbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #31.

Overlap of [3] abac=ab with [4] cabba=baabc:

Critical pair: ababaabc=ababba.

Flip LHS and RHS.

Defines rule #26.

Overlap of [4] cabba=baabc with [8] baabb=cc:

Critical pair: cabcc=baabcabb.

Reduce RHS:

Defines rule #4.

Referenced by [22], [23], [24], [25], [26], [27], [28], [29].

Overlap of [5] cbac=cb with [4] cabba=baabc:

Critical pair: cbabaabc=cbabba.

Flip LHS and RHS.

Defines rule #25.

Overlap of [6] abbac=abb with [4] cabba=baabc:

Critical pair: abbabaabc=abbabba.

Flip LHS and RHS.

Defines rule #35.

Overlap of [9] cca=c with [4] cabba=baabc:

Critical pair: cbaabc=cbba.

Flip LHS and RHS.

Defines rule #9.

Referenced by [33].

Overlap of [11] abca=ab with [4] cabba=baabc:

Critical pair: abbaabc=abbba.

Flip LHS and RHS.

Defines rule #24.

Referenced by [40].

Overlap of [3] abac=ab with [17] cabcc=ccb:

Critical pair: abaccb=ababcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [5] cbac=cb with [17] cabcc=ccb:

Critical pair: cbaccb=cbabcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [6] abbac=abb with [17] cabcc=ccb:

Critical pair: abbaccb=abbabcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #30.

Overlap of [9] cca=c with [17] cabcc=ccb:

Critical pair: cccb=cbcc.

Flip LHS and RHS.

Defines rule #3.

Referenced by [27], [36].

Overlap of [11] abca=ab with [17] cabcc=ccb:

Critical pair: abccb=abbcc.

Flip LHS and RHS.

Defines rule #14.

Referenced by [28], [37].

Overlap of [12] cbca=cb with [17] cabcc=ccb:

Critical pair: cbccb=cbbcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [13] abbca=abb with [17] cabcc=ccb:

Critical pair: abbccb=abbbcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Overlap of [17] cabcc=ccb with [9] cca=c:

Critical pair: cabc=ccba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [30], [31], [32], [33], [34].

Overlap of [3] abac=ab with [29] ccba=cabc:

Critical pair: abacabc=abcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [5] cbac=cb with [29] ccba=cabc:

Critical pair: cbacabc=cbcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [40].

Overlap of [6] abbac=abb with [29] ccba=cabc:

Critical pair: abbacabc=abbcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [7] cbbac=cbb with [29] ccba=cabc:

Critical pair: cbbacabc=cbbcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Overlap of [29] ccba=cabc with [8] baabb=cc:

Critical pair: cccc=cabcabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.

Referenced by [35], [36], [37], [38], [39].

Overlap of [3] abac=ab with [34] cabbb=cccc:

Critical pair: abacccc=ababbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #34.

Overlap of [5] cbac=cb with [34] cabbb=cccc:

Critical pair: cbacccc=cbabbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #33.

Overlap of [6] abbac=abb with [34] cabbb=cccc:

Critical pair: abbacccc=abbabbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #37.

Overlap of [9] cca=c with [34] cabbb=cccc:

Critical pair: ccccc=cbbb.

Flip LHS and RHS.

Defines rule #21.

Overlap of [11] abca=ab with [34] cabbb=cccc:

Critical pair: abcccc=abbbb.

Flip LHS and RHS.

Defines rule #32.

Overlap of [6] abbac=abb with [31] cbcba=cbabc:

Critical pair: abbacbabc=abbbcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #36.