Certificate for #4153 ⟨a, b | aabbaaaab=ba⟩

Completion settings:

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

Axiom: aabbaaaab=ba.

Referenced by [4].

Axiom: aaab=c.

Defines rule #6.

Referenced by [4], [6], [7].

Axiom: abba=d.

Referenced by [4], [5].

Overlap of [1] aabbaaaab=ba with [3] abba=d:

Critical pair: adaaab=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

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

Overlap of [3] abba=d with [4] ba=adc:

Critical pair: abadc=d.

Reduce LHS:

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

Overlap of [2] aaab=c with [4] ba=adc:

Critical pair: aaaadc=ca.

Referenced by [9], [12].

Overlap of [4] ba=adc with [2] aaab=c:

Critical pair: bc=adcaab.

Defines rule #7.

Overlap of [4] ba=adc with [5] aadcdc=d:

Critical pair: bd=adcadcdc.

Defines rule #8.

Overlap of [6] aaaadc=ca with [5] aadcdc=d:

Critical pair: aad=cadc.

Defines rule #3.

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

Overlap of [5] aadcdc=d with [9] aad=cadc:

Critical pair: cadccdc=d.

Defines rule #1.

Referenced by [11], [13].

Overlap of [5] aadcdc=d with [10] cadccdc=d:

Critical pair: aadcdd=dadccdc.

Reduce LHS:

Defines rule #2.

Overlap of [6] aaaadc=ca with [9] aad=cadc:

Critical pair: aacadcc=ca.

Defines rule #4.

Referenced by [13].

Overlap of [12] aacadcc=ca with [10] cadccdc=d:

Critical pair: aacadcd=caadccdc.

Reduce RHS:

Defines rule #5.