Certificate for #3190 ⟨a, b | abaaabababa=1⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(d) = deg(c) = 0, d < c; deg(a) = 1; deg(b) = 2
• Auxiliary generators:
  1. ba=c
  2. acaa=d

Axiom: abaaabababa=1.

Referenced by [4].

Axiom: ba=c.

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

Axiom: acaa=d.

Defines rule #8.

Referenced by [4], [5], [6], [14], [21].

Overlap of [1] abaaabababa=1 with [2] ba=c:

Critical pair: acaabababa=1.

Reduce LHS:

Referenced by [7], [8], [10], [11].

Overlap of [2] ba=c with [3] acaa=d:

Critical pair: bd=ccaa.

Referenced by [7].

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

Critical pair: acad=dcaa.

Referenced by [8], [15], [16].

Overlap of [5] bd=ccaa with [4] dccc=1:

Critical pair: b=ccaaccc.

Referenced by [9], [17].

Overlap of [6] acad=dcaa with [4] dccc=1:

Critical pair: aca=dcaaccc.

Flip LHS and RHS.

Referenced by [14], [18].

Overlap of [2] ba=c with [7] b=ccaaccc:

Critical pair: ccaaccca=c.

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

Overlap of [4] dccc=1 with [9] ccaaccca=c:

Critical pair: dcc=aaccca.

Flip LHS and RHS.

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

Overlap of [4] dccc=1 with [9] ccaaccca=c:

Critical pair: dccc=caaccca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [13], [20].

Overlap of [9] ccaaccca=c with [9] ccaaccca=c:

Critical pair: ccaacc=caccca.

Referenced by [17].

Overlap of [11] cdcc=1 with [9] ccaaccca=c:

Critical pair: cdc=aaccca.

Reduce RHS:

Flip LHS and RHS.

Referenced by [14].

Overlap of [13] dcc=cdc with [9] ccaaccca=c:

Critical pair: dc=cdcaaccca.

Reduce RHS:

Defines rule #1.

Referenced by [15], [16], [18], [19], [20], [23].

Overlap of [6] acad=dcaa with [14] dc=cd:

Critical pair: acacd=dcaac.

Reduce RHS:

Defines rule #5.

Simplify [6] acad=dcaa.

Reduce RHS:

Defines rule #3.

Simplify [7] b=ccaaccc.

Reduce RHS:

Referenced by [26].

Overlap of [8] dcaaccc=aca with [14] dc=cd:

Critical pair: cdaaccc=aca.

Referenced by [23].

Simplify [10] aaccca=dcc.

Reduce RHS:

Referenced by [21], [22].

Overlap of [11] cdcc=1 with [14] dc=cd:

Critical pair: ccdc=1.

Reduce LHS:

Defines rule #2.

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

Overlap of [3] acaa=d with [19] aaccca=ccd:

Critical pair: acaccd=daccca.

Defines rule #7.

Overlap of [19] aaccca=ccd with [19] aaccca=ccd:

Critical pair: aacccccd=ccdaccca.

Reduce LHS:

Defines rule #6.

Referenced by [23].

Simplify [18] cdaaccc=aca.

Reduce LHS:

Referenced by [24], [25].

Overlap of [20] cccd=1 with [23] dacccac=aca:

Critical pair: cccaca=acccac.

Flip LHS and RHS.

Defines rule #4.

Referenced by [25], [26].

Overlap of [23] dacccac=aca with [24] acccac=cccaca:

Critical pair: daccccccaca=acaccac.

Flip LHS and RHS.

Defines rule #9.

Simplify [17] b=cacccac.

Reduce RHS:

Defines rule #10.