Certificate for #4865 ⟨a, b | abbaabba=bab⟩

Completion settings:

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

Axiom: abbaabba=bab.

Referenced by [8].

Axiom: ab=c.

Defines rule #56.

Referenced by [9], [14], [15], [16], [21], [22].

Axiom: cc=d.

Defines rule #35.

Referenced by [12], [13], [22], [23], [40].

Axiom: bd=e.

Defines rule #29.

Referenced by [14], [19], [23], [33].

Axiom: ba=f.

Defines rule #30.

Referenced by [8], [9], [15], [16], [20].

Axiom: ff=g.

Defines rule #22.

Referenced by [10], [11], [17], [20], [25], [54], [60], [61].

Axiom: cf=h.

Defines rule #33.

Referenced by [9], [11], [13], [18], [24], [26], [35].

Simplify [1] abbaabba=bab.

Reduce RHS:

Referenced by [9].

Overlap of [8] abbaabba=fb with [2] ab=c:

Critical pair: cbaabba=fb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [16], [17], [18], [19], [20], [42].

Overlap of [6] ff=g with [6] ff=g:

Critical pair: fg=gf.

Flip LHS and RHS.

Referenced by [29].

Overlap of [7] cf=h with [6] ff=g:

Critical pair: cg=hf.

Defines rule #36.

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

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

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #49.

Referenced by [48], [54].

Overlap of [3] cc=d with [7] cf=h:

Critical pair: ch=df.

Flip LHS and RHS.

Defines rule #47.

Referenced by [42], [43], [44].

Overlap of [2] ab=c with [4] bd=e:

Critical pair: ae=cd.

Defines rule #53.

Overlap of [2] ab=c with [5] ba=f:

Critical pair: af=ca.

Defines rule #55.

Overlap of [5] ba=f with [2] ab=c:

Critical pair: bc=fb.

Reduce RHS:

Defines rule #27.

Referenced by [22], [23], [24], [34].

Overlap of [6] ff=g with [9] fb=hh:

Critical pair: fhh=gb.

Flip LHS and RHS.

Referenced by [21], [30].

Overlap of [7] cf=h with [9] fb=hh:

Critical pair: chh=hb.

Defines rule #6.

Referenced by [43], [48], [49], [50], [53], [54], [60], [61].

Overlap of [9] fb=hh with [4] bd=e:

Critical pair: fe=hhd.

Referenced by [25], [31].

Overlap of [9] fb=hh with [5] ba=f:

Critical pair: ff=hha.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [21], [27], [28], [37], [38], [46], [62].

Overlap of [20] hha=g with [2] ab=c:

Critical pair: hhc=gb.

Reduce RHS:

Referenced by [23], [32].

Overlap of [2] ab=c with [16] bc=hh:

Critical pair: ahh=cc.

Reduce RHS:

Defines rule #11.

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

Overlap of [16] bc=hh with [3] cc=d:

Critical pair: bd=hhc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [25], [26], [27], [28], [30], [32], [36], [43], [51].

Overlap of [16] bc=hh with [7] cf=h:

Critical pair: bh=hhf.

Defines rule #4.

Referenced by [43], [45], [46], [47], [49], [54], [60], [61].

Overlap of [6] ff=g with [23] fhh=e:

Critical pair: fe=ghh.

Reduce LHS:

Defines rule #10.

Referenced by [31], [56].

Overlap of [7] cf=h with [23] fhh=e:

Critical pair: ce=hhh.

Defines rule #31.

Referenced by [54], [55].

Overlap of [23] fhh=e with [20] hha=g:

Critical pair: fg=ea.

Defines rule #24.

Referenced by [29], [44].

Overlap of [23] fhh=e with [20] hha=g:

Critical pair: fhg=eha.

Defines rule #25.

Simplify [10] gf=fg.

Reduce RHS:

Defines rule #40.

Simplify [17] gb=fhh.

Reduce RHS:

Defines rule #42.

Referenced by [33], [34], [45].

Simplify [19] fe=hhd.

Reduce RHS:

Defines rule #20.

Simplify [21] hhc=fhh.

Reduce RHS:

Defines rule #7.

Referenced by [35], [36], [39], [41], [47], [49], [50], [63].

Overlap of [30] gb=e with [4] bd=e:

Critical pair: ge=ed.

Defines rule #38.

Referenced by [57].

Overlap of [30] gb=e with [16] bc=hh:

Critical pair: ghh=ec.

Flip LHS and RHS.

Defines rule #18.

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

Overlap of [32] hhc=e with [7] cf=h:

Critical pair: hhh=ef.

Flip LHS and RHS.

Defines rule #15.

Referenced by [51].

Overlap of [23] fhh=e with [32] hhc=e:

Critical pair: fhe=ehc.

Defines rule #21.

Overlap of [22] ahh=d with [20] hha=g:

Critical pair: ag=da.

Defines rule #57.

Overlap of [22] ahh=d with [20] hha=g:

Critical pair: ahg=dha.

Defines rule #58.

Overlap of [22] ahh=d with [32] hhc=e:

Critical pair: ahe=dhc.

Defines rule #54.

Overlap of [3] cc=d with [11] cg=hf:

Critical pair: chf=dg.

Flip LHS and RHS.

Defines rule #50.

Overlap of [32] hhc=e with [11] cg=hf:

Critical pair: hhhf=eg.

Flip LHS and RHS.

Defines rule #19.

Referenced by [58].

Overlap of [13] df=ch with [9] fb=hh:

Critical pair: dhh=chb.

Flip LHS and RHS.

Defines rule #34.

Referenced by [60], [61].

Overlap of [13] df=ch with [23] fhh=e:

Critical pair: de=chhh.

Reduce RHS:

Defines rule #44.

Referenced by [44], [54], [56], [57].

Overlap of [13] df=ch with [27] fg=ea:

Critical pair: dea=chg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #37.

Overlap of [30] gb=e with [24] bh=hhf:

Critical pair: ghhf=eh.

Defines rule #41.

Overlap of [24] bh=hhf with [20] hha=g:

Critical pair: bg=hhfha.

Defines rule #28.

Referenced by [61].

Overlap of [24] bh=hhf with [32] hhc=e:

Critical pair: be=hhfhc.

Defines rule #26.

Referenced by [60].

Overlap of [12] dc=cd with [18] chh=hb:

Critical pair: dhb=cdhh.

Defines rule #48.

Overlap of [18] chh=hb with [32] hhc=e:

Critical pair: che=hbhc.

Reduce RHS:

Defines rule #32.

Overlap of [32] hhc=e with [18] chh=hb:

Critical pair: hhhb=ehh.

Defines rule #5.

Overlap of [35] ef=hhh with [23] fhh=e:

Critical pair: ee=hhhhh.

Defines rule #13.

Referenced by [57], [58], [59], [64].

Overlap of [34] ec=ghh with [11] cg=hf:

Critical pair: ehf=ghhg.

Flip LHS and RHS.

Defines rule #43.

Overlap of [34] ec=ghh with [18] chh=hb:

Critical pair: ehb=ghhhh.

Defines rule #17.

Overlap of [12] dc=cd with [26] ce=hhh:

Critical pair: dhhh=cde.

Reduce RHS:

Defines rule #9.

Referenced by [62], [63].

Overlap of [34] ec=ghh with [26] ce=hhh:

Critical pair: ehhh=ghhe.

Flip LHS and RHS.

Defines rule #39.

Referenced by [56], [64].

Overlap of [25] hhd=ghh with [43] de=hhhf:

Critical pair: hhhhhf=ghhe.

Reduce RHS:

Defines rule #3.

Overlap of [33] ge=ed with [51] ee=hhhhh:

Critical pair: ghhhhh=ede.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [58].

Overlap of [51] ee=hhhhh with [41] eg=hhhf:

Critical pair: ehhhf=hhhhhg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [51] ee=hhhhh with [51] ee=hhhhh:

Critical pair: ehhhhh=hhhhhe.

Flip LHS and RHS.

Defines rule #1.

Overlap of [42] chb=dhh with [47] be=hhfhc:

Critical pair: chhhfhc=dhhe.

Reduce LHS:

Flip LHS and RHS.

Defines rule #46.

Overlap of [42] chb=dhh with [46] bg=hhfha:

Critical pair: chhhfha=dhhg.

Reduce LHS:

Flip LHS and RHS.

Defines rule #52.

Overlap of [54] dhhh=hhhg with [20] hha=g:

Critical pair: dhg=hhhga.

Defines rule #51.

Overlap of [54] dhhh=hhhg with [32] hhc=e:

Critical pair: dhe=hhhgc.

Defines rule #45.

Overlap of [55] ghhe=ehhh with [51] ee=hhhhh:

Critical pair: ghhhhhhh=ehhhe.

Flip LHS and RHS.

Defines rule #14.