Certificate for #5918 ⟨a, b | abbaab=ababa⟩

Completion settings:

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

Axiom: abbaab=ababa.

Referenced by [3].

Axiom: ababa=c.

Defines rule #23.

Referenced by [3], [4], [6], [7], [9], [16], [17], [32].

Simplify [1] abbaab=ababa.

Reduce RHS:

Defines rule #25.

Referenced by [5], [6], [7], [8], [13], [15], [20], [24], [26], [29].

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

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [8], [12], [13], [14], [23], [29], [30], [31].

Overlap of [3] abbaab=c with [3] abbaab=c:

Critical pair: abbac=cbaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [8], [9], [10], [13], [14], [21], [30].

Overlap of [3] abbaab=c with [2] ababa=c:

Critical pair: abbac=caba.

Flip LHS and RHS.

Defines rule #12.

Referenced by [10], [11], [12], [25].

Overlap of [2] ababa=c with [3] abbaab=c:

Critical pair: ababc=cbbaab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] abbaab=c with [5] abcab=abbac:

Critical pair: abbaabbac=ccab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [11], [14], [15], [17], [18], [19], [22], [28], [30], [31].

Overlap of [2] ababa=c with [5] abcab=abbac:

Critical pair: abababbac=cbcab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [12], [23], [30], [31].

Overlap of [5] abcab=abbac with [6] caba=abbac:

Critical pair: ababbac=abbaca.

Flip LHS and RHS.

Defines rule #26.

Referenced by [24], [25].

Overlap of [8] ccab=abcc with [6] caba=abbac:

Critical pair: cabbac=abcca.

Defines rule #13.

Referenced by [13], [14], [15], [18], [22], [24], [25], [27].

Overlap of [9] cbcab=cbbac with [6] caba=abbac:

Critical pair: cbabbac=cbbaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [5] abcab=abbac with [11] cabbac=abcca:

Critical pair: ababcca=abbacbac.

Reduce RHS:

Defines rule #24.

Referenced by [16], [17].

Overlap of [8] ccab=abcc with [11] cabbac=abcca:

Critical pair: cabcca=abccbac.

Reduce RHS:

Defines rule #14.

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

Overlap of [11] cabbac=abcca with [8] ccab=abcc:

Critical pair: cabbaabcc=abccacab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [20].

Overlap of [2] ababa=c with [13] ababcca=ccc:

Critical pair: abccc=cbcca.

Flip LHS and RHS.

Defines rule #6.

Referenced by [19].

Overlap of [13] ababcca=ccc with [8] ccab=abcc:

Critical pair: abababcc=cccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [18], [19], [30], [31].

Overlap of [11] cabbac=abcca with [17] cccb=cbcc:

Critical pair: cabbacbcc=abccaccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [17] cccb=cbcc with [16] cbcca=abccc:

Critical pair: ccabccc=cbcccca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [3] abbaab=c with [15] abccacab=cccc:

Critical pair: abbacccc=cccacab.

Flip LHS and RHS.

Defines rule #20.

Overlap of [5] abcab=abbac with [14] cabcca=abbaccc:

Critical pair: ababbaccc=abbaccca.

Flip LHS and RHS.

Defines rule #27.

Overlap of [8] ccab=abcc with [14] cabcca=abbaccc:

Critical pair: cabbaccc=abcccca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [26], [30].

Overlap of [9] cbcab=cbbac with [14] cabcca=abbaccc:

Critical pair: cbabbaccc=cbbaccca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [10] abbaca=ababbac with [11] cabbac=abcca:

Critical pair: abbaabcca=ababbacbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #32.

Referenced by [32], [33].

Overlap of [11] cabbac=abcca with [10] abbaca=ababbac:

Critical pair: cababbac=abccaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Referenced by [29], [30].

Overlap of [3] abbaab=c with [22] abcccca=abccacc:

Critical pair: abbaabccacc=ccccca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [27], [28], [31], [33].

Overlap of [11] cabbac=abcca with [26] ccccca=cccacc:

Critical pair: cabbacccacc=abccacccca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [26] ccccca=cccacc with [8] ccab=abcc:

Critical pair: cccabcc=cccaccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [3] abbaab=c with [25] abccaa=abbacbbac:

Critical pair: abbaabbacbbac=cccaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [31].

Overlap of [8] ccab=abcc with [25] abccaa=abbacbbac:

Critical pair: ccabbacbbac=abccccaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #30.

Referenced by [34].

Overlap of [26] ccccca=cccacc with [29] cccaa=abccbbac:

Critical pair: ccabccbbac=cccacca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [33].

Overlap of [2] ababa=c with [24] ababbacbbac=ccca:

Critical pair: abccca=cbbacbbac.

Flip LHS and RHS.

Defines rule #17.

Overlap of [24] ababbacbbac=ccca with [26] ccccca=cccacc:

Critical pair: ababbacbbacccacc=cccacccca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Simplify [27] abccacccca=abccaccacc.

Reduce RHS:

Defines rule #31.