Certificate for #4173 ⟨a, b | aabbabaab=ba⟩

Completion settings:

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

Axiom: aabbabaab=ba.

Referenced by [4].

Axiom: abba=c.

Referenced by [5], [6].

Axiom: ba=d.

Defines rule #7.

Referenced by [4], [5], [6], [7], [8], [9], [13].

Simplify [1] aabbabaab=ba.

Reduce RHS:

Referenced by [5].

Overlap of [4] aabbabaab=d with [2] abba=c:

Critical pair: acbaab=d.

Reduce LHS:

Defines rule #5.

Referenced by [8], [9], [10], [14].

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

Critical pair: abd=c.

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

Overlap of [3] ba=d with [6] abd=c:

Critical pair: bc=dbd.

Flip LHS and RHS.

Referenced by [12].

Overlap of [3] ba=d with [5] acdab=d:

Critical pair: bd=dcdab.

Defines rule #9.

Referenced by [11], [12].

Overlap of [5] acdab=d with [3] ba=d:

Critical pair: acdad=da.

Defines rule #3.

Overlap of [5] acdab=d with [6] abd=c:

Critical pair: acdc=dd.

Defines rule #1.

Overlap of [6] abd=c with [8] bd=dcdab:

Critical pair: adcdab=c.

Defines rule #6.

Referenced by [13], [14].

Overlap of [7] dbd=bc with [8] bd=dcdab:

Critical pair: ddcdab=bc.

Flip LHS and RHS.

Defines rule #8.

Overlap of [11] adcdab=c with [3] ba=d:

Critical pair: adcdad=ca.

Defines rule #4.

Referenced by [14].

Overlap of [13] adcdad=ca with [11] adcdab=c:

Critical pair: adcdc=cacdab.

Reduce RHS:

Defines rule #2.