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

Completion settings:

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

Axiom: aabbaab=aba.

Referenced by [7].

Axiom: ba=c.

Defines rule #69.

Referenced by [8], [12], [13], [16], [20].

Axiom: aabc=d.

Referenced by [9].

Axiom: bd=e.

Defines rule #46.

Referenced by [11], [15], [16], [20].

Axiom: cc=f.

Defines rule #38.

Referenced by [10], [14], [16], [17], [21], [25], [28], [33], [35].

Axiom: ab=g.

Defines rule #62.

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

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], [23].

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

Critical pair: agc=d.

Defines rule #61.

Referenced by [13], [20], [21], [22], [23], [26], [37].

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

Critical pair: cf=fc.

Flip LHS and RHS.

Defines rule #15.

Referenced by [30], [35], [42].

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

Critical pair: ae=gd.

Defines rule #56.

Referenced by [19], [27], [31], [44], [45], [66].

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

Critical pair: bg=cb.

Flip LHS and RHS.

Defines rule #50.

Referenced by [14], [15], [18], [22], [29], [34], [60].

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

Critical pair: ac=ga.

Reduce RHS:

Defines rule #60.

Referenced by [16], [17], [18], [27], [38], [44], [45].

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

Critical pair: cbg=fb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #48.

Overlap of [12] cb=bg with [4] bd=e:

Critical pair: ce=bgd.

Flip LHS and RHS.

Defines rule #47.

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

Critical pair: bdg=cc.

Reduce LHS:

Reduce RHS:

Defines rule #3.

Referenced by [19], [30], [32], [35], [36], [39], [40], [41], [43], [48], [63], [64], [69].

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

Critical pair: af=dgc.

Referenced by [19], [24].

Overlap of [13] ac=dg with [12] cb=bg:

Critical pair: abg=dgb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #49.

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

Critical pair: af=gdg.

Reduce LHS:

Defines rule #32.

Referenced by [24], [26].

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

Critical pair: bd=cgc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #45.

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

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

Critical pair: agf=dc.

Defines rule #59.

Referenced by [51], [52], [53], [54], [63], [67].

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

Critical pair: agbg=db.

Defines rule #63.

Simplify [8] ga=agcg.

Reduce RHS:

Defines rule #65.

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

Simplify [17] af=dgc.

Reduce RHS:

Defines rule #57.

Referenced by [66].

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

Critical pair: ce=fgc.

Flip LHS and RHS.

Defines rule #31.

Referenced by [33], [34], [35], [42], [59], [75].

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

Critical pair: age=dgc.

Reduce RHS:

Defines rule #58.

Referenced by [51], [52], [54], [63], [67].

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

Critical pair: ae=dggc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #44.

Referenced by [60], [61].

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

Critical pair: cgf=ec.

Defines rule #34.

Referenced by [40], [44], [68].

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

Critical pair: cgbg=eb.

Defines rule #54.

Referenced by [62], [74].

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

Critical pair: cge=egc.

Reduce RHS:

Defines rule #33.

Referenced by [37], [38], [39], [40], [68].

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

Critical pair: ggd=dge.

Referenced by [47].

Overlap of [16] eg=f with [23] ga=dg:

Critical pair: edg=fa.

Flip LHS and RHS.

Defines rule #64.

Referenced by [52], [53], [71].

Overlap of [25] fgc=ce with [5] cc=f:

Critical pair: fgf=cec.

Flip LHS and RHS.

Defines rule #39.

Referenced by [59], [61], [62].

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

Critical pair: fgbg=ceb.

Flip LHS and RHS.

Defines rule #51.

Overlap of [25] fgc=ce with [20] cgc=e:

Critical pair: fge=cegc.

Reduce RHS:

Defines rule #4.

Referenced by [36].

Overlap of [35] fge=ff with [16] eg=f:

Critical pair: fgf=ffg.

Flip LHS and RHS.

Defines rule #8.

Referenced by [50].

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

Critical pair: agcf=dge.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [43], [47], [67], [71], [72], [73].

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

Critical pair: acf=dgge.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [20] cgc=e with [30] cge=cf:

Critical pair: cgcf=ege.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [41], [51], [68], [72], [73].

Overlap of [30] cge=cf with [16] eg=f:

Critical pair: cgf=cfg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #35.

Referenced by [45], [46], [49], [55].

Overlap of [39] fe=ef with [16] eg=f:

Critical pair: ff=efg.

Flip LHS and RHS.

Defines rule #7.

Referenced by [42], [50], [56].

Overlap of [41] efg=ff with [25] fgc=ce:

Critical pair: ece=ffc.

Reduce RHS:

Defines rule #12.

Overlap of [37] dge=df with [16] eg=f:

Critical pair: dgf=dfg.

Flip LHS and RHS.

Defines rule #11.

Referenced by [57], [58], [70].

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

Critical pair: aec=dggf.

Reduce LHS:

Defines rule #30.

Referenced by [45], [74].

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

Critical pair: aec=dgfg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [57].

Overlap of [40] cfg=ec with [23] ga=dg:

Critical pair: cfdg=eca.

Flip LHS and RHS.

Defines rule #66.

Simplify [31] ggd=dge.

Reduce RHS:

Defines rule #23.

Referenced by [48], [49], [50], [57], [65].

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

Critical pair: edf=fgd.

Flip LHS and RHS.

Defines rule #5.

Referenced by [54], [55], [56], [58], [70].

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

Critical pair: cfdf=ecgd.

Flip LHS and RHS.

Defines rule #36.

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

Critical pair: efdf=ffgd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [21] agf=dc with [39] fe=ef:

Critical pair: agef=dce.

Reduce LHS:

Defines rule #24.

Referenced by [66], [69], [70], [71], [72], [73].

Overlap of [21] agf=dc with [32] fa=edg:

Critical pair: agedg=dca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #67.

Overlap of [32] fa=edg with [21] agf=dc:

Critical pair: fdc=edggf.

Flip LHS and RHS.

Defines rule #28.

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

Critical pair: agedf=dcgd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #37.

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

Critical pair: cedf=ecd.

Flip LHS and RHS.

Defines rule #13.

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

Critical pair: eedf=ffd.

Flip LHS and RHS.

Defines rule #2.

Referenced by [66], [67], [68], [73].

Overlap of [43] dfg=dgf with [47] ggd=df:

Critical pair: dfdf=dgfgd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #26.

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

Critical pair: dedf=dgfd.

Flip LHS and RHS.

Defines rule #10.

Overlap of [25] fgc=ce with [33] cec=fgf:

Critical pair: fgfgf=ceec.

Flip LHS and RHS.

Defines rule #40.

Referenced by [75].

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

Critical pair: dggbg=gdb.

Defines rule #53.

Overlap of [27] dggc=gd with [33] cec=fgf:

Critical pair: dggfgf=gdec.

Defines rule #43.

Overlap of [33] cec=fgf with [29] cgbg=eb:

Critical pair: ceeb=fgfgbg.

Flip LHS and RHS.

Defines rule #52.

Overlap of [26] age=gdg with [16] eg=f:

Critical pair: agf=gdgg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #41.

Referenced by [64], [65].

Overlap of [16] eg=f with [63] gdgg=dc:

Critical pair: edc=fdgg.

Flip LHS and RHS.

Defines rule #29.

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

Critical pair: gddf=dcd.

Flip LHS and RHS.

Defines rule #17.

Overlap of [24] af=gdg with [56] ffd=eedf:

Critical pair: aeedf=gdgfd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [21] agf=dc with [56] ffd=eedf:

Critical pair: ageedf=dcfd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [28] cgf=ec with [56] ffd=eedf:

Critical pair: cgeedf=ecfd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

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

Critical pair: edce=fdgf.

Defines rule #21.

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

Critical pair: fdce=edfgf.

Reduce RHS:

Defines rule #22.

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

Critical pair: gdgedg=dcea.

Reduce LHS:

Flip LHS and RHS.

Defines rule #68.

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

Critical pair: gdgef=dcee.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

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

Critical pair: gdgeedf=dcefd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [44] gdc=dggf with [29] cgbg=eb:

Critical pair: gdeb=dggfgbg.

Flip LHS and RHS.

Defines rule #55.

Overlap of [25] fgc=ce with [59] ceec=fgfgf:

Critical pair: fgfgfgf=ceeec.

Defines rule #42.