Certificate for #2255 ⟨a, b | aabbaab=aba⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(e) = deg(f) = 0, e < f; deg(c) = deg(g) = deg(d) = 1, c < g < d; deg(a) = deg(b) = 2, a < b
• Auxiliary generators:
  1. ba=c
  2. aabc=d
  3. bd=e
  4. cc=f
  5. ab=g

Axiom: aabbaab=aba.

Referenced by [7].

Axiom: ba=c.

Defines rule #65.

Referenced by [8], [12], [13], [14], [15], [18].

Axiom: aabc=d.

Referenced by [9].

Axiom: bd=e.

Defines rule #54.

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

Axiom: cc=f.

Defines rule #9.

Referenced by [10], [15], [16], [19], [20], [23], [30], [33], [40].

Axiom: ab=g.

Defines rule #63.

Referenced by [7], [8], [9], [11], [12], [13], [27].

Simplify [1] aabbaab=aba.

Reduce RHS:

Referenced by [8].

Overlap of [7] aabbaab=ga with [6] ab=g:

Critical pair: agbaab=ga.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [25].

Overlap of [3] aabc=d with [6] ab=g:

Critical pair: agc=d.

Defines rule #48.

Referenced by [13], [18], [19], [21], [25], [31], [34], [41].

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

Critical pair: cf=fc.

Flip LHS and RHS.

Defines rule #3.

Referenced by [24].

Overlap of [6] ab=g with [4] bd=e:

Critical pair: ae=gd.

Defines rule #43.

Referenced by [14], [17], [22], [28], [42], [44], [53], [63].

Overlap of [2] ba=c with [6] ab=g:

Critical pair: bg=cb.

Flip LHS and RHS.

Defines rule #57.

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

Overlap of [6] ab=g with [2] ba=c:

Critical pair: ac=ga.

Reduce RHS:

Defines rule #45.

Referenced by [15], [16], [22], [35], [42], [44], [53].

Overlap of [2] ba=c with [11] ae=gd:

Critical pair: bgd=ce.

Defines rule #55.

Overlap of [2] ba=c with [13] ac=dg:

Critical pair: bdg=cc.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [17], [24], [29], [36], [37], [38], [39], [48], [60], [61], [66].

Overlap of [13] ac=dg with [5] cc=f:

Critical pair: af=dgc.

Referenced by [17], [26].

Overlap of [11] ae=gd with [15] eg=f:

Critical pair: af=gdg.

Reduce LHS:

Defines rule #34.

Referenced by [21], [26], [41].

Overlap of [2] ba=c with [9] agc=d:

Critical pair: bd=cgc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [20], [21], [22], [23], [24], [32], [36].

Overlap of [9] agc=d with [5] cc=f:

Critical pair: agf=dc.

Defines rule #47.

Referenced by [51], [52], [55], [60], [64].

Overlap of [5] cc=f with [18] cgc=e:

Critical pair: ce=fgc.

Flip LHS and RHS.

Defines rule #16.

Referenced by [46], [54].

Overlap of [9] agc=d with [18] cgc=e:

Critical pair: age=dgc.

Reduce RHS:

Defines rule #46.

Referenced by [41], [51], [52], [55], [60], [64].

Overlap of [13] ac=dg with [18] cgc=e:

Critical pair: ae=dggc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #42.

Referenced by [59].

Overlap of [18] cgc=e with [5] cc=f:

Critical pair: cgf=ec.

Defines rule #12.

Referenced by [37], [40], [41], [42], [43], [65].

Overlap of [18] cgc=e with [18] cgc=e:

Critical pair: cge=egc.

Reduce RHS:

Defines rule #11.

Referenced by [33], [34], [35], [36], [37], [43], [65].

Simplify [8] ga=agcg.

Reduce RHS:

Defines rule #51.

Referenced by [27], [28], [29], [45].

Simplify [16] af=dgc.

Reduce RHS:

Defines rule #44.

Referenced by [63].

Overlap of [25] ga=dg with [6] ab=g:

Critical pair: gg=dgb.

Flip LHS and RHS.

Defines rule #61.

Referenced by [69].

Overlap of [25] ga=dg with [11] ae=gd:

Critical pair: ggd=dge.

Referenced by [41], [47].

Overlap of [15] eg=f with [25] ga=dg:

Critical pair: edg=fa.

Flip LHS and RHS.

Defines rule #49.

Referenced by [52], [68].

Overlap of [5] cc=f with [12] cb=bg:

Critical pair: cbg=fb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #56.

Referenced by [69].

Overlap of [9] agc=d with [12] cb=bg:

Critical pair: agbg=db.

Defines rule #64.

Overlap of [18] cgc=e with [12] cb=bg:

Critical pair: cgbg=eb.

Defines rule #59.

Overlap of [5] cc=f with [24] cge=cf:

Critical pair: ccf=fge.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [39].

Overlap of [9] agc=d with [24] cge=cf:

Critical pair: agcf=dge.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [41], [47], [64], [68], [70], [71].

Overlap of [13] ac=dg with [24] cge=cf:

Critical pair: acf=dgge.

Reduce LHS:

Flip LHS and RHS.

Defines rule #35.

Overlap of [18] cgc=e with [24] cge=cf:

Critical pair: cgcf=ege.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [38], [43], [51], [65], [70], [71].

Overlap of [24] cge=cf with [15] eg=f:

Critical pair: cgf=cfg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [44], [45], [49], [56].

Overlap of [36] fe=ef with [15] eg=f:

Critical pair: ff=efg.

Flip LHS and RHS.

Defines rule #6.

Referenced by [50], [57].

Overlap of [33] fge=ff with [15] eg=f:

Critical pair: fgf=ffg.

Flip LHS and RHS.

Defines rule #7.

Referenced by [50].

Overlap of [5] cc=f with [23] cgf=ec:

Critical pair: cec=fgf.

Defines rule #10.

Referenced by [54].

Overlap of [9] agc=d with [23] cgf=ec:

Critical pair: agec=dgf.

Reduce LHS:

Defines rule #22.

Referenced by [58], [67].

Overlap of [13] ac=dg with [23] cgf=ec:

Critical pair: aec=dggf.

Reduce LHS:

Flip LHS and RHS.

Defines rule #36.

Overlap of [23] cgf=ec with [36] fe=ef:

Critical pair: cgef=ece.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [53].

Overlap of [13] ac=dg with [37] cfg=ec:

Critical pair: aec=dgfg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #37.

Overlap of [37] cfg=ec with [25] ga=dg:

Critical pair: cfdg=eca.

Flip LHS and RHS.

Defines rule #50.

Overlap of [20] fgc=ce with [12] cb=bg:

Critical pair: fgbg=ceb.

Defines rule #58.

Simplify [28] ggd=dge.

Reduce RHS:

Defines rule #27.

Referenced by [48], [49], [50], [62].

Overlap of [15] eg=f with [47] ggd=df:

Critical pair: edf=fgd.

Flip LHS and RHS.

Defines rule #18.

Referenced by [55], [56], [57], [58], [67].

Overlap of [37] cfg=ec with [47] ggd=df:

Critical pair: cfdf=ecgd.

Flip LHS and RHS.

Defines rule #26.

Overlap of [38] efg=ff with [47] ggd=df:

Critical pair: efdf=ffgd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [19] agf=dc with [36] fe=ef:

Critical pair: agef=dce.

Reduce LHS:

Defines rule #29.

Referenced by [63], [66], [67], [68], [69], [70], [71].

Overlap of [19] agf=dc with [29] fa=edg:

Critical pair: agedg=dca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #52.

Overlap of [11] ae=gd with [43] ece=cff:

Critical pair: acff=gdce.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [20] fgc=ce with [40] cec=fgf:

Critical pair: fgfgf=ceec.

Defines rule #17.

Overlap of [19] agf=dc with [48] fgd=edf:

Critical pair: agedf=dcgd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #41.

Overlap of [37] cfg=ec with [48] fgd=edf:

Critical pair: cedf=ecd.

Flip LHS and RHS.

Defines rule #14.

Overlap of [38] efg=ff with [48] fgd=edf:

Critical pair: eedf=ffd.

Flip LHS and RHS.

Defines rule #8.

Referenced by [63], [64], [65], [71].

Overlap of [41] dfg=dgf with [48] fgd=edf:

Critical pair: dedf=dgfd.

Flip LHS and RHS.

Defines rule #39.

Overlap of [22] dggc=gd with [12] cb=bg:

Critical pair: dggbg=gdb.

Defines rule #62.

Overlap of [21] age=gdg with [15] eg=f:

Critical pair: agf=gdgg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #40.

Referenced by [61], [62].

Overlap of [15] eg=f with [60] gdgg=dc:

Critical pair: edc=fdgg.

Flip LHS and RHS.

Defines rule #38.

Overlap of [60] gdgg=dc with [47] ggd=df:

Critical pair: gddf=dcd.

Flip LHS and RHS.

Defines rule #30.

Overlap of [26] af=gdg with [57] ffd=eedf:

Critical pair: aeedf=gdgfd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #31.

Overlap of [19] agf=dc with [57] ffd=eedf:

Critical pair: ageedf=dcfd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #32.

Overlap of [23] cgf=ec with [57] ffd=eedf:

Critical pair: cgeedf=ecfd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [15] eg=f with [51] gdgf=dce:

Critical pair: edce=fdgf.

Flip LHS and RHS.

Defines rule #24.

Overlap of [48] fgd=edf with [51] gdgf=dce:

Critical pair: fdce=edfgf.

Reduce RHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [51] gdgf=dce with [29] fa=edg:

Critical pair: gdgedg=dcea.

Reduce LHS:

Flip LHS and RHS.

Defines rule #53.

Overlap of [51] gdgf=dce with [30] fb=bgg:

Critical pair: gdgbgg=dceb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #60.

Overlap of [51] gdgf=dce with [36] fe=ef:

Critical pair: gdgef=dcee.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [51] gdgf=dce with [57] ffd=eedf:

Critical pair: gdgeedf=dcefd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #33.