Certificate for #4342 ⟨a, b | abbabaaab=ba⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(d) = deg(e) = deg(f) = 0, d < e < f; deg(c) = 1; deg(a) = 2; deg(b) = 3
• Auxiliary generators:
  1. ba=c
  2. bcc=d
  3. aab=e
  4. cedec=f

Axiom: abbabaaab=ba.

Referenced by [6].

Axiom: ba=c.

Defines rule #42.

Referenced by [6], [7], [8], [9], [10].

Axiom: bcc=d.

Referenced by [7], [11].

Axiom: aab=e.

Defines rule #37.

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

Axiom: cedec=f.

Defines rule #13.

Referenced by [15], [16], [17], [18], [20], [21], [26], [29], [31], [34], [36], [38], [40], [46], [47], [48].

Simplify [1] abbabaaab=ba.

Reduce RHS:

Referenced by [7].

Overlap of [6] abbabaaab=c with [2] ba=c:

Critical pair: abcbaaab=c.

Reduce LHS:

Referenced by [8], [13], [19], [22].

Overlap of [2] ba=c with [7] ade=c:

Critical pair: bc=cde.

Defines rule #41.

Referenced by [11], [14], [18].

Overlap of [2] ba=c with [4] aab=e:

Critical pair: be=cab.

Defines rule #39.

Overlap of [4] aab=e with [2] ba=c:

Critical pair: aac=ea.

Referenced by [13], [23].

Simplify [3] bcc=d.

Reduce LHS:

Defines rule #12.

Referenced by [12], [13], [14], [15], [16], [20], [25], [28], [30], [33], [35], [37], [39], [42], [43], [45], [47].

Overlap of [11] cdec=d with [11] cdec=d:

Critical pair: cded=ddec.

Defines rule #5.

Referenced by [14].

Overlap of [10] aac=ea with [11] cdec=d:

Critical pair: aad=eadec.

Reduce RHS:

Referenced by [19], [24].

Overlap of [8] bc=cde with [11] cdec=d:

Critical pair: bd=cdedec.

Reduce RHS:

Defines rule #38.

Overlap of [11] cdec=d with [5] cedec=f:

Critical pair: cdef=dedec.

Defines rule #7.

Overlap of [5] cedec=f with [11] cdec=d:

Critical pair: ceded=fdec.

Defines rule #8.

Overlap of [5] cedec=f with [5] cedec=f:

Critical pair: cedef=fedec.

Defines rule #9.

Overlap of [8] bc=cde with [5] cedec=f:

Critical pair: bf=cdeedec.

Defines rule #40.

Overlap of [13] aad=ecc with [7] ade=c:

Critical pair: ac=ecce.

Defines rule #24.

Referenced by [20], [21], [23], [32].

Overlap of [19] ac=ecce with [11] cdec=d:

Critical pair: ad=eccedec.

Reduce RHS:

Defines rule #21.

Referenced by [22], [24].

Overlap of [19] ac=ecce with [5] cedec=f:

Critical pair: af=ecceedec.

Defines rule #22.

Overlap of [7] ade=c with [20] ad=ecf:

Critical pair: ecfe=c.

Defines rule #2.

Referenced by [25], [26], [27], [32].

Overlap of [10] aac=ea with [19] ac=ecce:

Critical pair: aecce=ea.

Defines rule #31.

Referenced by [32].

Overlap of [13] aad=ecc with [20] ad=ecf:

Critical pair: aecf=ecc.

Defines rule #26.

Overlap of [11] cdec=d with [22] ecfe=c:

Critical pair: cdc=dfe.

Defines rule #10.

Referenced by [28], [29].

Overlap of [5] cedec=f with [22] ecfe=c:

Critical pair: cedc=ffe.

Defines rule #11.

Referenced by [30], [31].

Overlap of [22] ecfe=c with [22] ecfe=c:

Critical pair: ecfc=ccfe.

Flip LHS and RHS.

Defines rule #16.

Referenced by [33], [34], [41], [44].

Overlap of [25] cdc=dfe with [11] cdec=d:

Critical pair: cdd=dfedec.

Defines rule #1.

Overlap of [25] cdc=dfe with [5] cedec=f:

Critical pair: cdf=dfeedec.

Defines rule #3.

Overlap of [26] cedc=ffe with [11] cdec=d:

Critical pair: cedd=ffedec.

Defines rule #4.

Overlap of [26] cedc=ffe with [5] cedec=f:

Critical pair: cedf=ffeedec.

Defines rule #6.

Overlap of [23] aecce=ea with [22] ecfe=c:

Critical pair: aeccc=eacfe.

Reduce RHS:

Defines rule #35.

Referenced by [39], [40], [41].

Overlap of [11] cdec=d with [27] ccfe=ecfc:

Critical pair: cdeecfc=dcfe.

Defines rule #19.

Referenced by [35], [36].

Overlap of [5] cedec=f with [27] ccfe=ecfc:

Critical pair: cedeecfc=fcfe.

Defines rule #20.

Referenced by [37], [38].

Overlap of [33] cdeecfc=dcfe with [11] cdec=d:

Critical pair: cdeecfd=dcfedec.

Defines rule #14.

Overlap of [33] cdeecfc=dcfe with [5] cedec=f:

Critical pair: cdeecff=dcfeedec.

Defines rule #17.

Overlap of [34] cedeecfc=fcfe with [11] cdec=d:

Critical pair: cedeecfd=fcfedec.

Defines rule #15.

Overlap of [34] cedeecfc=fcfe with [5] cedec=f:

Critical pair: cedeecff=fcfeedec.

Defines rule #18.

Overlap of [32] aeccc=eeccefe with [11] cdec=d:

Critical pair: aeccd=eeccefedec.

Defines rule #30.

Referenced by [42].

Overlap of [32] aeccc=eeccefe with [5] cedec=f:

Critical pair: aeccf=eeccefeedec.

Defines rule #32.

Referenced by [44].

Overlap of [32] aeccc=eeccefe with [27] ccfe=ecfc:

Critical pair: aececfc=eeccefefe.

Defines rule #36.

Referenced by [45], [46].

Overlap of [39] aeccd=eeccefedec with [11] cdec=d:

Critical pair: aecd=eeccefedecec.

Defines rule #25.

Referenced by [43].

Overlap of [42] aecd=eeccefedecec with [11] cdec=d:

Critical pair: aed=eeccefedececec.

Defines rule #23.

Overlap of [40] aeccf=eeccefeedec with [27] ccfe=ecfc:

Critical pair: aeecfc=eeccefeedece.

Defines rule #29.

Referenced by [47], [48].

Overlap of [41] aececfc=eeccefefe with [11] cdec=d:

Critical pair: aececfd=eeccefefedec.

Defines rule #33.

Overlap of [41] aececfc=eeccefefe with [5] cedec=f:

Critical pair: aececff=eeccefefeedec.

Defines rule #34.

Overlap of [44] aeecfc=eeccefeedece with [11] cdec=d:

Critical pair: aeecfd=eeccefeedecedec.

Reduce RHS:

Defines rule #27.

Overlap of [44] aeecfc=eeccefeedece with [5] cedec=f:

Critical pair: aeecff=eeccefeedeceedec.

Defines rule #28.