Certificate for #3536 ⟨a, b | aabaaaaaba=b⟩

Completion settings:

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

Axiom: aabaaaaaba=b.

Referenced by [3].

Axiom: aa=c.

Defines rule #6.

Referenced by [3], [4], [5], [10], [13], [14], [16], [17], [18].

Overlap of [1] aabaaaaaba=b with [2] aa=c:

Critical pair: cbaaaaaba=b.

Reduce LHS:

Defines rule #7.

Referenced by [5], [6], [8].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [6], [7], [10], [11], [13], [14], [16], [17], [18].

Overlap of [3] cbccaba=b with [2] aa=c:

Critical pair: cbccabc=ba.

Defines rule #5.

Referenced by [7], [8], [9], [10], [12], [15].

Overlap of [4] ac=ca with [3] cbccaba=b:

Critical pair: ab=cabccaba.

Flip LHS and RHS.

Defines rule #17.

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

Overlap of [4] ac=ca with [5] cbccabc=ba:

Critical pair: aba=cabccabc.

Flip LHS and RHS.

Defines rule #15.

Overlap of [5] cbccabc=ba with [3] cbccaba=b:

Critical pair: cbccabb=babccaba.

Flip LHS and RHS.

Defines rule #16.

Referenced by [16], [17], [18].

Overlap of [5] cbccabc=ba with [5] cbccabc=ba:

Critical pair: cbccabba=babccabc.

Flip LHS and RHS.

Defines rule #14.

Overlap of [5] cbccabc=ba with [6] cabccaba=ab:

Critical pair: cbcab=bacaba.

Reduce RHS:

Defines rule #2.

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

Overlap of [4] ac=ca with [10] cbcab=bccba:

Critical pair: abccba=cabcab.

Flip LHS and RHS.

Defines rule #11.

Referenced by [14].

Overlap of [5] cbccabc=ba with [10] cbcab=bccba:

Critical pair: cbccabbccba=babcab.

Flip LHS and RHS.

Defines rule #10.

Overlap of [10] cbcab=bccba with [6] cabccaba=ab:

Critical pair: cbab=bccbaccaba.

Reduce RHS:

Defines rule #1.

Referenced by [15], [16].

Overlap of [11] cabcab=abccba with [6] cabccaba=ab:

Critical pair: cabab=abccbaccaba.

Reduce RHS:

Defines rule #9.

Referenced by [17].

Overlap of [5] cbccabc=ba with [13] cbab=bccbcccba:

Critical pair: cbccabbccbcccba=babab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [18].

Overlap of [13] cbab=bccbcccba with [8] babccaba=cbccabb:

Critical pair: ccbccabb=bccbcccbaccaba.

Reduce RHS:

Defines rule #4.

Overlap of [14] cabab=abccbcccba with [8] babccaba=cbccabb:

Critical pair: cacbccabb=abccbcccbaccaba.

Reduce LHS:

Reduce RHS:

Defines rule #13.

Overlap of [15] babab=cbccabbccbcccba with [8] babccaba=cbccabb:

Critical pair: bacbccabb=cbccabbccbcccbaccaba.

Reduce LHS:

Reduce RHS:

Defines rule #12.