Certificate for #4675 ⟨a, b | aababbba=baa⟩

Completion settings:

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

Axiom: aababbba=baa.

Referenced by [5].

Axiom: ababbb=c.

Defines rule #23.

Referenced by [5], [7], [8], [9], [12], [13].

Axiom: ccc=d.

Defines rule #17.

Referenced by [6], [9], [10], [12], [13], [15], [17], [19], [20], [21], [25].

Axiom: cad=e.

Defines rule #15.

Referenced by [9], [11], [13], [22], [23], [24], [26].

Overlap of [1] aababbba=baa with [2] ababbb=c:

Critical pair: aca=baa.

Flip LHS and RHS.

Defines rule #19.

Referenced by [7], [8], [9], [12], [13], [14], [15].

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

Critical pair: cd=dc.

Defines rule #14.

Overlap of [2] ababbb=c with [5] baa=aca:

Critical pair: ababbaca=caa.

Referenced by [15].

Overlap of [5] baa=aca with [2] ababbb=c:

Critical pair: bac=acababbb.

Reduce RHS:

Defines rule #22.

Referenced by [9], [10], [11], [12], [15].

Overlap of [2] ababbb=c with [8] bac=acc:

Critical pair: ababbacc=cac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [12], [15], [20].

Overlap of [8] bac=acc with [3] ccc=d:

Critical pair: bad=acccc.

Reduce RHS:

Defines rule #21.

Referenced by [13].

Overlap of [8] bac=acc with [4] cad=e:

Critical pair: bae=accad.

Reduce RHS:

Referenced by [12], [27].

Overlap of [2] ababbb=c with [11] bae=ace:

Critical pair: ababbace=cae.

Reduce LHS:

Flip LHS and RHS.

Referenced by [14], [16].

Overlap of [2] ababbb=c with [10] bad=adc:

Critical pair: ababbadc=cad.

Reduce LHS:

Reduce RHS:

Defines rule #3.

Referenced by [14], [15], [16], [18].

Overlap of [5] baa=aca with [13] aaed=e:

Critical pair: be=acaed.

Reduce RHS:

Defines rule #18.

Overlap of [7] ababbaca=caa with [8] bac=acc:

Critical pair: ababacca=caa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [17], [18], [19], [20], [21], [22], [23], [24], [26].

Simplify [12] cae=aaaaede.

Reduce RHS:

Defines rule #13.

Referenced by [19].

Overlap of [3] ccc=d with [15] caa=aaea:

Critical pair: ccaaea=daa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [22].

Overlap of [15] caa=aaea with [13] aaed=e:

Critical pair: ce=aaeaed.

Defines rule #11.

Referenced by [21], [27].

Overlap of [3] ccc=d with [16] cae=aaee:

Critical pair: ccaaee=dae.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [23].

Overlap of [3] ccc=d with [9] cac=aaec:

Critical pair: ccaaec=dac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [24], [25].

Overlap of [3] ccc=d with [18] ce=aaeaed:

Critical pair: ccaaeaed=de.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [4] cad=e with [17] daa=aaeaeaea:

Critical pair: caaaeaeaea=eaa.

Reduce LHS:

Defines rule #1.

Overlap of [4] cad=e with [19] dae=aaeaeaee:

Critical pair: caaaeaeaee=eae.

Reduce LHS:

Defines rule #2.

Overlap of [4] cad=e with [20] dac=aaeaeaec:

Critical pair: caaaeaeaec=eac.

Reduce LHS:

Defines rule #9.

Overlap of [20] dac=aaeaeaec with [3] ccc=d:

Critical pair: dad=aaeaeaeccc.

Reduce RHS:

Defines rule #8.

Referenced by [26].

Overlap of [4] cad=e with [25] dad=aaeaeaed:

Critical pair: caaaeaeaed=ead.

Reduce LHS:

Defines rule #4.

Simplify [11] bae=ace.

Reduce RHS:

Defines rule #20.