Certificate for #4097 ⟨a, b | aabaabbaa=ab⟩

Completion settings:

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

Axiom: aabaabbaa=ab.

Referenced by [3].

Axiom: bbaa=c.

Defines rule #5.

Referenced by [3], [4], [5], [8], [11], [12], [14], [15], [17], [18].

Overlap of [1] aabaabbaa=ab with [2] bbaa=c:

Critical pair: aabaac=ab.

Defines rule #1.

Referenced by [4], [5], [6], [17].

Overlap of [2] bbaa=c with [3] aabaac=ab:

Critical pair: bbab=cbaac.

Defines rule #17.

Referenced by [8], [9], [10], [13], [16].

Overlap of [2] bbaa=c with [3] aabaac=ab:

Critical pair: bbaab=cabaac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [6], [7], [9], [10], [18].

Overlap of [3] aabaac=ab with [5] cabaac=cb:

Critical pair: aabaacb=ababaac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [9], [19].

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

Critical pair: cabaacb=cbabaac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [10], [20].

Overlap of [4] bbab=cbaac with [2] bbaa=c:

Critical pair: bbac=cbaacbaa.

Defines rule #10.

Overlap of [6] ababaac=abb with [5] cabaac=cb:

Critical pair: ababaacb=abbabaac.

Reduce LHS:

Reduce RHS:

Defines rule #15.

Referenced by [11], [12], [13], [19].

Overlap of [5] cabaac=cb with [7] cbabaac=cbb:

Critical pair: cabaacbb=cbbabaac.

Reduce LHS:

Reduce RHS:

Defines rule #16.

Referenced by [14], [15], [16], [20].

Overlap of [9] abbb=acbaacaac with [2] bbaa=c:

Critical pair: abc=acbaacaacaa.

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [9] abbb=acbaacaac with [2] bbaa=c:

Critical pair: abbc=acbaacaacbaa.

Defines rule #6.

Overlap of [9] abbb=acbaacaac with [4] bbab=cbaac:

Critical pair: abcbaac=acbaacaacab.

Defines rule #13.

Overlap of [10] cbbb=ccbaacaac with [2] bbaa=c:

Critical pair: cbc=ccbaacaacaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [20], [22].

Overlap of [10] cbbb=ccbaacaac with [2] bbaa=c:

Critical pair: cbbc=ccbaacaacbaa.

Defines rule #7.

Overlap of [10] cbbb=ccbaacaac with [4] bbab=cbaac:

Critical pair: cbcbaac=ccbaacaacab.

Defines rule #14.

Overlap of [3] aabaac=ab with [11] acbaacaacaa=abc:

Critical pair: aabaabc=abbaacaacaa.

Reduce RHS:

Defines rule #8.

Referenced by [21], [22].

Overlap of [5] cabaac=cb with [11] acbaacaacaa=abc:

Critical pair: cabaabc=cbbaacaacaa.

Reduce RHS:

Defines rule #9.

Overlap of [6] ababaac=abb with [11] acbaacaacaa=abc:

Critical pair: ababaabc=abbbaacaacaa.

Reduce RHS:

Defines rule #18.

Overlap of [7] cbabaac=cbb with [11] acbaacaacaa=abc:

Critical pair: cbabaabc=cbbbaacaacaa.

Reduce RHS:

Defines rule #19.

Overlap of [11] acbaacaacaa=abc with [17] aabaabc=accaacaa:

Critical pair: acbaacaacaccaacaa=abcbaabc.

Flip LHS and RHS.

Defines rule #20.

Overlap of [14] ccbaacaacaa=cbc with [17] aabaabc=accaacaa:

Critical pair: ccbaacaacaccaacaa=cbcbaabc.

Flip LHS and RHS.

Defines rule #21.