Certificate for #1587 ⟨a, b | aaaababaa=a⟩

Completion settings:

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

Axiom: aaaababaa=a.

Referenced by [3].

Axiom: ababa=c.

Defines rule #8.

Referenced by [3], [4], [5], [6], [7].

Overlap of [1] aaaababaa=a with [2] ababa=c:

Critical pair: aaaca=a.

Referenced by [5], [6], [8], [10], [11], [14].

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

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [9], [15].

Overlap of [2] ababa=c with [3] aaaca=a:

Critical pair: ababa=caaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [10].

Overlap of [3] aaaca=a with [2] ababa=c:

Critical pair: aaacc=ababa.

Reduce RHS:

Defines rule #3.

Referenced by [7], [9], [11].

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

Critical pair: ababc=caacc.

Referenced by [13].

Overlap of [3] aaaca=a with [5] caaca=c:

Critical pair: aaac=aaca.

Flip LHS and RHS.

Referenced by [10], [11], [14].

Overlap of [4] cba=abc with [6] aaacc=c:

Critical pair: cbc=abcaacc.

Referenced by [12].

Overlap of [8] aaca=aaac with [5] caaca=c:

Critical pair: aac=aaacaca.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [8] aaca=aaac with [10] aca=aac:

Critical pair: aacaac=aaacca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [12], [13], [16], [17], [18], [19].

Simplify [9] cbc=abcaacc.

Reduce RHS:

Defines rule #5.

Simplify [7] ababc=caacc.

Reduce RHS:

Defines rule #9.

Overlap of [3] aaaca=a with [8] aaca=aaac:

Critical pair: aaaac=a.

Defines rule #2.

Referenced by [15], [19].

Overlap of [14] aaaac=a with [4] cba=abc:

Critical pair: aaaaabc=aba.

Defines rule #7.

Referenced by [16].

Overlap of [15] aaaaabc=aba with [11] ca=ac:

Critical pair: aaaaabac=abaa.

Referenced by [17].

Overlap of [16] aaaaabac=abaa with [11] ca=ac:

Critical pair: aaaaabaac=abaaa.

Referenced by [18].

Overlap of [17] aaaaabaac=abaaa with [11] ca=ac:

Critical pair: aaaaabaaac=abaaaa.

Referenced by [19].

Overlap of [18] aaaaabaaac=abaaaa with [11] ca=ac:

Critical pair: aaaaabaaaac=abaaaaa.

Reduce LHS:

Defines rule #6.