Certificate for #5655 ⟨a, b | aabaab=ababa⟩

Completion settings:

• Auxiliary generators:
  1. c = ab
  2. d = cccc
• Reduction order:
  • Left-to-right recursive path with deg(a) = deg(d) = 0, a < d; deg(c) = deg(b) = 1, c < b

Axiom: aabaab=ababa.

Referenced by [4].

Axiom: ab=c.

Defines rule #3.

Referenced by [4], [5], [9].

Axiom: cccc=d.

Defines rule #10.

Referenced by [6], [7], [9], [10], [12], [13], [15], [16], [17], [18].

Simplify [1] aabaab=ababa.

Reduce RHS:

Referenced by [5].

Overlap of [4] aabaab=cca with [2] ab=c:

Critical pair: acaab=cca.

Reduce LHS:

Defines rule #4.

Referenced by [7], [8], [10], [11], [12], [14], [16], [18].

Overlap of [3] cccc=d with [3] cccc=d:

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #1.

Referenced by [10].

Overlap of [5] acac=cca with [3] cccc=d:

Critical pair: acad=ccaccc.

Flip LHS and RHS.

Defines rule #13.

Referenced by [12], [13].

Overlap of [5] acac=cca with [5] acac=cca:

Critical pair: accca=ccaac.

Defines rule #7.

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

Overlap of [8] accca=ccaac with [2] ab=c:

Critical pair: acccc=ccaacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [11].

Overlap of [8] accca=ccaac with [5] acac=cca:

Critical pair: accccca=ccaaccac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [14].

Overlap of [5] acac=cca with [9] ccaacb=ad:

Critical pair: acaad=ccacaacb.

Flip LHS and RHS.

Defines rule #15.

Referenced by [15], [16].

Overlap of [5] acac=cca with [7] ccaccc=acad:

Critical pair: acaacad=ccacaccc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [7] ccaccc=acad with [8] accca=ccaac:

Critical pair: ccccaac=acada.

Reduce LHS:

Defines rule #2.

Overlap of [5] acac=cca with [10] ccaaccac=acda:

Critical pair: acaacda=ccacaaccac.

Flip LHS and RHS.

Defines rule #16.

Referenced by [17], [18].

Overlap of [3] cccc=d with [11] ccacaacb=acaad:

Critical pair: ccacaad=dacaacb.

Flip LHS and RHS.

Defines rule #9.

Overlap of [5] acac=cca with [11] ccacaacb=acaad:

Critical pair: acaacaad=ccacacaacb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [3] cccc=d with [14] ccacaaccac=acaacda:

Critical pair: ccacaacda=dacaaccac.

Flip LHS and RHS.

Defines rule #11.

Overlap of [5] acac=cca with [14] ccacaaccac=acaacda:

Critical pair: acaacaacda=ccacacaaccac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.