Certificate for #5298 ⟨a, b | abaaaba=aaab⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(c) = deg(e) = deg(f) = 0, c < e < f; deg(d) = deg(a) = 1, d < a; deg(b) = 2
• Auxiliary generators:
  1. aa=c
  2. ba=d
  3. dcd=e
  4. ddce=f

Axiom: abaaaba=aaab.

Referenced by [6].

Axiom: aa=c.

Defines rule #23.

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

Axiom: ba=d.

Defines rule #25.

Referenced by [7], [9], [14], [15], [16], [18], [27].

Axiom: dcd=e.

Defines rule #21.

Referenced by [7], [10], [11], [17], [18], [19], [21], [24], [28], [30], [31], [33], [38], [40], [42].

Axiom: ddce=f.

Defines rule #19.

Referenced by [11], [24], [25], [28], [29], [30], [31], [34], [39], [40], [41], [42], [43].

Simplify [1] abaaaba=aaab.

Reduce RHS:

Referenced by [7].

Overlap of [6] abaaaba=cab with [3] ba=d:

Critical pair: adaaba=cab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #16.

Referenced by [12].

Overlap of [3] ba=d with [2] aa=c:

Critical pair: bc=da.

Defines rule #24.

Referenced by [19].

Overlap of [4] dcd=e with [4] dcd=e:

Critical pair: dce=ecd.

Flip LHS and RHS.

Defines rule #12.

Referenced by [28], [29], [40], [41], [42], [43].

Overlap of [4] dcd=e with [5] ddce=f:

Critical pair: dcf=edce.

Flip LHS and RHS.

Referenced by [32].

Simplify [7] cab=ae.

Reduce LHS:

Defines rule #32.

Referenced by [13], [14], [15].

Overlap of [2] aa=c with [12] acb=ae:

Critical pair: aae=ccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Referenced by [16].

Overlap of [3] ba=d with [12] acb=ae:

Critical pair: bae=dcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #31.

Referenced by [17], [18], [19].

Overlap of [12] acb=ae with [3] ba=d:

Critical pair: acd=aea.

Flip LHS and RHS.

Referenced by [22].

Overlap of [13] ccb=ce with [3] ba=d:

Critical pair: ccd=cea.

Flip LHS and RHS.

Referenced by [23].

Overlap of [4] dcd=e with [14] dcb=de:

Critical pair: dcde=ecb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [25], [26].

Overlap of [14] dcb=de with [3] ba=d:

Critical pair: dcd=dea.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [14] dcb=de with [9] bc=da:

Critical pair: dcda=dec.

Reduce LHS:

Defines rule #17.

Referenced by [20], [22], [23], [24], [27].

Simplify [18] dea=e.

Reduce LHS:

Defines rule #20.

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

Overlap of [4] dcd=e with [20] ddec=e:

Critical pair: dce=edec.

Flip LHS and RHS.

Referenced by [35].

Overlap of [15] aea=acd with [19] ea=dec:

Critical pair: adec=acd.

Flip LHS and RHS.

Defines rule #22.

Referenced by [42], [43].

Overlap of [16] cea=ccd with [19] ea=dec:

Critical pair: cdec=ccd.

Flip LHS and RHS.

Defines rule #11.

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

Overlap of [5] ddce=f with [19] ea=dec:

Critical pair: ddcdec=fa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [5] ddce=f with [17] ecb=ee:

Critical pair: ddcee=fcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #30.

Referenced by [27].

Overlap of [20] ddec=e with [17] ecb=ee:

Critical pair: ddee=eb.

Flip LHS and RHS.

Defines rule #26.

Referenced by [31].

Overlap of [25] fcb=fe with [3] ba=d:

Critical pair: fcd=fea.

Reduce RHS:

Referenced by [28], [36].

Overlap of [5] ddce=f with [10] ecd=dce:

Critical pair: ddcdce=fcd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [20] ddec=e with [10] ecd=dce:

Critical pair: dddce=ed.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

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

Overlap of [5] ddce=f with [29] ed=df:

Critical pair: ddcdf=fd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [36], [37].

Overlap of [5] ddce=f with [26] eb=ddee:

Critical pair: ddcddee=fb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Simplify [11] edce=dcf.

Reduce LHS:

Defines rule #7.

Referenced by [33].

Overlap of [4] dcd=e with [32] dfce=dcf:

Critical pair: dcdcf=efce.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [34].

Overlap of [5] ddce=f with [33] efce=ecf:

Critical pair: ddcecf=ffce.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [21] edec=dce with [29] ed=df:

Critical pair: dfec=dce.

Defines rule #8.

Referenced by [38].

Simplify [27] fcd=fdec.

Reduce RHS:

Referenced by [44].

Overlap of [28] fdec=dece with [30] fd=def:

Critical pair: defec=dece.

Referenced by [44].

Overlap of [4] dcd=e with [35] dfec=dce:

Critical pair: dcdce=efec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [39].

Overlap of [5] ddce=f with [38] efec=ece:

Critical pair: ddcece=ffec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [23] ccd=cdec with [4] dcd=e:

Critical pair: cce=cdeccd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [23] ccd=cdec with [5] ddce=f:

Critical pair: ccf=cdecdce.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [22] acd=adec with [4] dcd=e:

Critical pair: ace=adeccd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [22] acd=adec with [5] ddce=f:

Critical pair: acf=adecdce.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Simplify [36] fcd=defec.

Reduce RHS:

Defines rule #13.