Certificate for #3200 ⟨a, b | abaabaaaaab=1⟩

Completion settings:

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

Axiom: abaabaaaaab=1.

Referenced by [3].

Axiom: aba=c.

Referenced by [3], [4], [5], [9], [14], [18], [21].

Overlap of [1] abaabaaaaab=1 with [2] aba=c:

Critical pair: cabaaaaab=1.

Reduce LHS:

Referenced by [5], [7].

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

Critical pair: abc=cba.

Flip LHS and RHS.

Referenced by [10], [18], [19].

Overlap of [3] ccaaaab=1 with [2] aba=c:

Critical pair: ccaaac=a.

Defines rule #2.

Referenced by [6], [8], [12], [13], [20], [22], [23].

Overlap of [5] ccaaac=a with [5] ccaaac=a:

Critical pair: ccaaaa=acaaac.

Defines rule #1.

Referenced by [7], [11], [13], [18], [23].

Overlap of [3] ccaaaab=1 with [6] ccaaaa=acaaac:

Critical pair: acaaacb=1.

Referenced by [8], [13], [14].

Overlap of [5] ccaaac=a with [7] acaaacb=1:

Critical pair: ccaa=aaaacb.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [2] aba=c with [8] aaaacb=ccaa:

Critical pair: abccaa=caaacb.

Flip LHS and RHS.

Referenced by [12], [14], [23].

Overlap of [8] aaaacb=ccaa with [4] cba=abc:

Critical pair: aaaaabc=ccaaa.

Referenced by [11].

Overlap of [6] ccaaaa=acaaac with [10] aaaaabc=ccaaa:

Critical pair: ccccaaa=acaaacabc.

Flip LHS and RHS.

Referenced by [19].

Overlap of [5] ccaaac=a with [9] caaacb=abccaa:

Critical pair: cabccaa=ab.

Referenced by [13], [14], [15].

Overlap of [5] ccaaac=a with [12] cabccaa=ab:

Critical pair: ccaaaab=aabccaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16], [17], [21], [23].

Overlap of [12] cabccaa=ab with [7] acaaacb=1:

Critical pair: cabcca=abcaaacb.

Reduce RHS:

Referenced by [15].

Overlap of [12] cabccaa=ab with [14] cabcca=cbccaa:

Critical pair: cbccaaa=ab.

Referenced by [18], [21].

Overlap of [13] aabccaa=1 with [13] aabccaa=1:

Critical pair: aabcc=bccaa.

Referenced by [17].

Overlap of [13] aabccaa=1 with [13] aabccaa=1:

Critical pair: aabcca=abccaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [15] cbccaaa=ab with [6] ccaaaa=acaaac:

Critical pair: cbacaaac=aba.

Reduce LHS:

Reduce RHS:

Referenced by [19], [20].

Overlap of [18] bacaaacc=c with [4] cba=abc:

Critical pair: bacaaacabc=cba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [18] bacaaacc=c with [5] ccaaac=a:

Critical pair: bacaaaa=caaac.

Defines rule #3.

Overlap of [19] abc=bccccaaa with [15] cbccaaa=ab:

Critical pair: abab=bccccaaabccaaa.

Reduce LHS:

Reduce RHS:

Defines rule #6.

Referenced by [22], [23].

Overlap of [5] ccaaac=a with [21] cb=bccccaa:

Critical pair: ccaaabccccaa=ab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [23].

Overlap of [6] ccaaaa=acaaac with [22] ab=bccccaaccaaa:

Critical pair: ccaaabccccaaccaaa=acaaacb.

Reduce LHS:

Reduce RHS:

Defines rule #4.