Certificate for #4727 ⟨a, b | aabbbaba=baa⟩

Completion settings:

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

Axiom: aabbbaba=baa.

Referenced by [4].

Axiom: abbbab=c.

Defines rule #22.

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

Axiom: ccca=d.

Defines rule #10.

Referenced by [7], [9], [10], [11], [12], [13], [14], [15], [16], [17], [21], [22], [23], [24], [28], [32].

Overlap of [1] aabbbaba=baa with [2] abbbab=c:

Critical pair: aca=baa.

Flip LHS and RHS.

Defines rule #13.

Referenced by [6], [8], [9], [11], [24], [29], [30], [31].

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

Critical pair: abbbc=cbbab.

Defines rule #19.

Referenced by [22], [23].

Overlap of [2] abbbab=c with [4] baa=aca:

Critical pair: abbbaaca=caa.

Reduce LHS:

Referenced by [17].

Overlap of [3] ccca=d with [2] abbbab=c:

Critical pair: cccc=dbbbab.

Flip LHS and RHS.

Defines rule #23.

Referenced by [24].

Overlap of [4] baa=aca with [2] abbbab=c:

Critical pair: bac=acabbbab.

Reduce RHS:

Defines rule #17.

Referenced by [9], [10], [11], [17], [24].

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

Critical pair: abbbaacc=cac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [13].

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

Critical pair: bad=acccca.

Reduce RHS:

Defines rule #15.

Referenced by [11].

Overlap of [2] abbbab=c with [10] bad=acd:

Critical pair: abbbaacd=cad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [12], [18], [19], [20], [21], [25], [26], [27], [28], [29], [30], [31].

Overlap of [3] ccca=d with [11] cad=aadcd:

Critical pair: ccaadcd=dd.

Referenced by [14], [18].

Overlap of [3] ccca=d with [9] cac=aadcc:

Critical pair: ccaadcc=dc.

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

Overlap of [3] ccca=d with [12] ccaadcd=dd:

Critical pair: cdd=dadcd.

Defines rule #6.

Referenced by [20], [29], [30], [31].

Overlap of [3] ccca=d with [13] ccaadcc=dc:

Critical pair: cdc=dadcc.

Defines rule #8.

Referenced by [18], [19], [20], [21], [25], [26], [27], [28], [30], [31].

Overlap of [13] ccaadcc=dc with [3] ccca=d:

Critical pair: ccaadd=dcca.

Referenced by [20].

Overlap of [6] abbacaca=caa with [8] bac=acc:

Critical pair: abaccaca=caa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [18], [19], [20], [21], [29], [30], [31].

Overlap of [12] ccaadcd=dd with [17] caa=aadca:

Critical pair: caadcadcd=dd.

Reduce LHS:

Referenced by [25].

Overlap of [13] ccaadcc=dc with [17] caa=aadca:

Critical pair: caadcadcc=dc.

Reduce LHS:

Referenced by [26].

Overlap of [16] ccaadd=dcca with [17] caa=aadca:

Critical pair: caadcadd=dcca.

Reduce LHS:

Referenced by [27].

Overlap of [3] ccca=d with [17] caa=aadca:

Critical pair: ccaadca=da.

Reduce LHS:

Referenced by [28].

Overlap of [3] ccca=d with [5] abbbc=cbbab:

Critical pair: ccccbbab=dbbbc.

Flip LHS and RHS.

Defines rule #20.

Overlap of [5] abbbc=cbbab with [3] ccca=d:

Critical pair: abbbd=cbbabcca.

Flip LHS and RHS.

Defines rule #21.

Overlap of [7] dbbbab=cccc with [4] baa=aca:

Critical pair: dbbbaaca=ccccaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [25], [26], [27], [28], [29], [30], [31].

Overlap of [18] aadaaddadaadaaddadcdadccd=dd with [24] cda=dadca:

Critical pair: aadaaddadaadaaddaddadcadccd=dd.

Reduce LHS:

Defines rule #11.

Referenced by [30].

Overlap of [19] aadaaddadaadaaddadcdadccc=dc with [24] cda=dadca:

Critical pair: aadaaddadaadaaddaddadcadccc=dc.

Reduce LHS:

Defines rule #12.

Referenced by [30], [31], [32].

Overlap of [20] aadaaddadaadaaddadcdadcd=dcca with [24] cda=dadca:

Critical pair: aadaaddadaadaaddaddadcadcd=dcca.

Reduce LHS:

Defines rule #9.

Overlap of [21] aadaaddadaadaaddadcdadcca=da with [24] cda=dadca:

Critical pair: aadaaddadaadaaddaddadcadcca=da.

Reduce LHS:

Defines rule #1.

Referenced by [29], [30], [31].

Overlap of [4] baa=aca with [28] aadaaddadaadaaddaddadaaddadd=da:

Critical pair: bda=acadaaddadaadaaddaddadaaddadd.

Reduce RHS:

Referenced by [33].

Overlap of [4] baa=aca with [25] aadaaddadaadaaddaddadaaddadcccd=dd:

Critical pair: bdd=acadaaddadaadaaddaddadaaddadcccd.

Reduce RHS:

Defines rule #16.

Overlap of [4] baa=aca with [26] aadaaddadaadaaddaddadaaddadcccc=dc:

Critical pair: bdc=acadaaddadaadaaddaddadaaddadcccc.

Reduce RHS:

Defines rule #18.

Overlap of [26] aadaaddadaadaaddaddadaaddadcccc=dc with [3] ccca=d:

Critical pair: aadaaddadaadaaddaddadaaddadcd=dca.

Defines rule #2.

Referenced by [33].

Simplify [29] bda=aaaddadaadaaddaddadaaddaddaadaaddadaadaaddaddadaaddadcd.

Reduce RHS:

Defines rule #14.