Certificate for #3374 ⟨a, b | aaaabaabaa=a⟩

Completion settings:

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

Axiom: aaaabaabaa=a.

Referenced by [3].

Axiom: abaab=c.

Defines rule #9.

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

Overlap of [1] aaaabaabaa=a with [2] abaab=c:

Critical pair: aaacaa=a.

Referenced by [5], [6], [7], [8], [9], [10], [11], [12], [13], [18].

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

Critical pair: abac=caab.

Flip LHS and RHS.

Referenced by [8], [14].

Overlap of [3] aaacaa=a with [2] abaab=c:

Critical pair: aaacac=abaab.

Reduce RHS:

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

Overlap of [3] aaacaa=a with [3] aaacaa=a:

Critical pair: aaaca=aacaa.

Flip LHS and RHS.

Referenced by [10], [11], [12], [13], [16], [18].

Overlap of [3] aaacaa=a with [5] aaacac=c:

Critical pair: aaacc=aacac.

Flip LHS and RHS.

Referenced by [19].

Overlap of [3] aaacaa=a with [4] caab=abac:

Critical pair: aaaabac=ab.

Referenced by [9], [13], [15], [16], [27].

Overlap of [3] aaacaa=a with [8] aaaabac=ab:

Critical pair: aaacab=aaabac.

Referenced by [16].

Overlap of [3] aaacaa=a with [6] aacaa=aaaca:

Critical pair: aaacaaaca=acaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [6] aacaa=aaaca with [5] aaacac=c:

Critical pair: aacc=aaacaacac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [6] aacaa=aaaca with [6] aacaa=aaaca:

Critical pair: aacaaaca=aaacacaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [14], [15], [16], [17], [20], [21], [22], [23], [24], [25], [26], [28], [29].

Overlap of [6] aacaa=aaaca with [8] aaaabac=ab:

Critical pair: aacab=aaacaaabac.

Reduce RHS:

Referenced by [17].

Overlap of [4] caab=abac with [12] caa=aca:

Critical pair: acab=abac.

Defines rule #7.

Referenced by [17], [20].

Overlap of [8] aaaabac=ab with [12] caa=aca:

Critical pair: aaaabaaca=abaa.

Referenced by [22].

Overlap of [12] caa=aca with [8] aaaabac=ab:

Critical pair: cab=acaaabac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [20], [21].

Overlap of [14] acab=abac with [2] abaab=c:

Critical pair: acc=abacaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [3] aaacaa=a with [6] aacaa=aaaca:

Critical pair: aaaaca=a.

Defines rule #3.

Referenced by [26].

Overlap of [5] aaacac=c with [7] aacac=aaacc:

Critical pair: aaaacc=c.

Defines rule #4.

Referenced by [23].

Overlap of [12] caa=aca with [16] aaabaacc=cab:

Critical pair: ccab=acaabaacc.

Reduce RHS:

Defines rule #8.

Overlap of [16] aaabaacc=cab with [12] caa=aca:

Critical pair: aaabaacaca=cabaa.

Reduce LHS:

Referenced by [23].

Overlap of [15] aaaabaaca=abaa with [12] caa=aca:

Critical pair: aaaabaaaca=abaaa.

Referenced by [26].

Overlap of [21] aaabaaacca=cabaa with [12] caa=aca:

Critical pair: aaabaaacaca=cabaaa.

Reduce LHS:

Referenced by [24].

Overlap of [23] aaabca=cabaaa with [12] caa=aca:

Critical pair: aaabaca=cabaaaa.

Referenced by [25].

Overlap of [24] aaabaca=cabaaaa with [12] caa=aca:

Critical pair: aaabaaca=cabaaaaa.

Referenced by [28].

Overlap of [22] aaaabaaaca=abaaa with [12] caa=aca:

Critical pair: aaaabaaaaca=abaaaa.

Reduce LHS:

Referenced by [27].

Overlap of [8] aaaabac=ab with [26] aaaaba=abaaaa:

Critical pair: abaaaac=ab.

Defines rule #5.

Referenced by [29], [30].

Overlap of [25] aaabaaca=cabaaaaa with [12] caa=aca:

Critical pair: aaabaaaca=cabaaaaaa.

Referenced by [29].

Overlap of [28] aaabaaaca=cabaaaaaa with [12] caa=aca:

Critical pair: aaabaaaaca=cabaaaaaaa.

Reduce LHS:

Referenced by [30].

Overlap of [29] aaaba=cabaaaaaaa with [27] abaaaac=ab:

Critical pair: aaab=cabaaaaaaaaaac.

Defines rule #6.