Certificate for #5283 ⟨a, b | abaaaab=aaba⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with c < a < b < d < e
• Auxiliary generators:
  1. ba=c
  2. caa=d
  3. ada=e

Axiom: abaaaab=aaba.

Referenced by [5].

Axiom: ba=c.

Defines rule #1.

Referenced by [5], [6], [7], [10], [14], [17], [18], [24], [32], [35], [36], [42], [44], [51], [53], [56], [62], [64], [66].

Axiom: caa=d.

Defines rule #3.

Referenced by [6], [8], [11], [12], [14], [20], [25], [54], [65].

Axiom: ada=e.

Defines rule #8.

Referenced by [6], [7], [8], [9], [13], [20], [26], [43], [45], [48], [51].

Simplify [1] abaaaab=aaba.

Reduce RHS:

Referenced by [6].

Overlap of [5] abaaaab=aac with [2] ba=c:

Critical pair: acaaab=aac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [10], [11], [12], [13], [14], [15], [16], [19], [27], [28], [29], [30], [31], [32], [53], [63], [72].

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

Critical pair: be=cda.

Flip LHS and RHS.

Defines rule #4.

Referenced by [15], [16], [44], [47].

Overlap of [3] caa=d with [4] ada=e:

Critical pair: cae=dda.

Flip LHS and RHS.

Defines rule #12.

Referenced by [19], [48], [49].

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

Critical pair: ade=eda.

Flip LHS and RHS.

Referenced by [21].

Overlap of [2] ba=c with [6] aac=eb:

Critical pair: beb=cac.

Defines rule #10.

Referenced by [18].

Overlap of [3] caa=d with [6] aac=eb:

Critical pair: ceb=dc.

Defines rule #6.

Referenced by [17].

Overlap of [3] caa=d with [6] aac=eb:

Critical pair: caeb=dac.

Defines rule #17.

Referenced by [35], [40].

Overlap of [4] ada=e with [6] aac=eb:

Critical pair: adeb=eac.

Defines rule #20.

Referenced by [36], [37], [38], [39], [41], [53].

Overlap of [6] aac=eb with [3] caa=d:

Critical pair: aad=ebaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [20], [23], [37], [43], [44], [45], [47], [48], [49].

Overlap of [6] aac=eb with [7] cda=be:

Critical pair: aabe=ebda.

Flip LHS and RHS.

Defines rule #31.

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

Overlap of [7] cda=be with [6] aac=eb:

Critical pair: cdeb=beac.

Flip LHS and RHS.

Defines rule #23.

Referenced by [40], [41], [42], [55], [66], [72].

Overlap of [11] ceb=dc with [2] ba=c:

Critical pair: cec=dca.

Flip LHS and RHS.

Defines rule #11.

Referenced by [23], [33], [38], [67], [72].

Overlap of [10] beb=cac with [2] ba=c:

Critical pair: bec=caca.

Flip LHS and RHS.

Defines rule #16.

Referenced by [32], [33], [34], [39], [42], [46], [50], [68].

Overlap of [8] dda=cae with [6] aac=eb:

Critical pair: ddeb=caeac.

Flip LHS and RHS.

Referenced by [22].

Overlap of [14] eca=aad with [3] caa=d:

Critical pair: ed=aada.

Reduce RHS:

Defines rule #2.

Referenced by [21], [23], [26], [45], [48], [49], [52], [53].

Overlap of [9] eda=ade with [20] ed=ae:

Critical pair: aea=ade.

Defines rule #9.

Referenced by [22], [24], [25], [26], [27], [45], [48], [49].

Overlap of [19] caeac=ddeb with [21] aea=ade:

Critical pair: cadec=ddeb.

Referenced by [47], [57].

Overlap of [20] ed=ae with [17] dca=cec:

Critical pair: ecec=aeca.

Reduce RHS:

Defines rule #29.

Referenced by [71].

Overlap of [2] ba=c with [21] aea=ade:

Critical pair: bade=cea.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [28], [29], [37], [38], [39], [40], [41], [47].

Overlap of [3] caa=d with [21] aea=ade:

Critical pair: caade=dea.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [27], [29], [30], [48], [49], [53].

Overlap of [4] ada=e with [21] aea=ade:

Critical pair: adade=eea.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [31], [49], [56], [62], [64].

Overlap of [21] aea=ade with [6] aac=eb:

Critical pair: aeeb=adeac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [58].

Overlap of [6] aac=eb with [24] cea=cde:

Critical pair: aacde=ebea.

Reduce LHS:

Flip LHS and RHS.

Defines rule #32.

Referenced by [55].

Overlap of [24] cea=cde with [6] aac=eb:

Critical pair: ceeb=cdeac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [59].

Overlap of [25] dea=dde with [6] aac=eb:

Critical pair: deeb=ddeac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [60].

Overlap of [26] eea=aee with [6] aac=eb:

Critical pair: eeeb=aeeac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [52].

Overlap of [6] aac=eb with [18] caca=bec:

Critical pair: aabec=ebaca.

Reduce RHS:

Defines rule #39.

Referenced by [54].

Overlap of [17] dca=cec with [18] caca=bec:

Critical pair: dbec=cecca.

Flip LHS and RHS.

Defines rule #37.

Overlap of [18] caca=bec with [18] caca=bec:

Critical pair: cabec=becca.

Flip LHS and RHS.

Defines rule #41.

Overlap of [12] caeb=dac with [2] ba=c:

Critical pair: caec=daca.

Flip LHS and RHS.

Defines rule #24.

Referenced by [43], [44], [45], [46], [54], [69].

Overlap of [13] adeb=eac with [2] ba=c:

Critical pair: adec=eaca.

Flip LHS and RHS.

Defines rule #30.

Referenced by [47], [48], [49], [50], [70].

Overlap of [14] eca=aad with [13] adeb=eac:

Critical pair: eceac=aaddeb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [61].

Overlap of [17] dca=cec with [13] adeb=eac:

Critical pair: dceac=cecdeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #49.

Overlap of [18] caca=bec with [13] adeb=eac:

Critical pair: caceac=becdeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #53.

Overlap of [12] caeb=dac with [16] beac=cdeb:

Critical pair: caecdeb=daceac.

Reduce RHS:

Defines rule #57.

Overlap of [13] adeb=eac with [16] beac=cdeb:

Critical pair: adecdeb=eaceac.

Reduce RHS:

Defines rule #59.

Overlap of [16] beac=cdeb with [18] caca=bec:

Critical pair: beabec=cdebaca.

Reduce RHS:

Defines rule #54.

Overlap of [4] ada=e with [35] daca=caec:

Critical pair: acaec=eca.

Reduce RHS:

Defines rule #38.

Overlap of [7] cda=be with [35] daca=caec:

Critical pair: ccaec=beca.

Reduce RHS:

Defines rule #35.

Overlap of [20] ed=ae with [35] daca=caec:

Critical pair: ecaec=aeaca.

Reduce LHS:

Reduce RHS:

Defines rule #40.

Overlap of [35] daca=caec with [18] caca=bec:

Critical pair: dabec=caecca.

Flip LHS and RHS.

Defines rule #47.

Overlap of [24] cea=cde with [36] eaca=adec:

Critical pair: cadec=cdeca.

Reduce LHS:

Reduce RHS:

Defines rule #26.

Referenced by [51], [57], [61].

Overlap of [25] dea=dde with [36] eaca=adec:

Critical pair: dadec=ddeca.

Reduce RHS:

Defines rule #42.

Overlap of [26] eea=aee with [36] eaca=adec:

Critical pair: eadec=aeeca.

Reduce RHS:

Defines rule #43.

Overlap of [36] eaca=adec with [18] caca=bec:

Critical pair: eabec=adecca.

Flip LHS and RHS.

Defines rule #51.

Overlap of [47] ddeb=bead with [2] ba=c:

Critical pair: ddec=beada.

Reduce RHS:

Defines rule #25.

Referenced by [52], [53], [58], [59], [60], [73].

Overlap of [20] ed=ae with [51] ddec=bee:

Critical pair: ebee=aedec.

Reduce RHS:

Flip LHS and RHS.

Defines rule #34.

Referenced by [56].

Overlap of [15] ebda=aabe with [13] adeb=eac:

Critical pair: ebdeac=aabedeb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #46.

Overlap of [15] ebda=aabe with [35] daca=caec:

Critical pair: ebcaec=aabeca.

Reduce RHS:

Defines rule #55.

Overlap of [28] ebea=ebde with [16] beac=cdeb:

Critical pair: ecdeb=ebdec.

Flip LHS and RHS.

Defines rule #44.

Referenced by [71].

Overlap of [52] eeeb=ebee with [2] ba=c:

Critical pair: eeec=ebeea.

Reduce RHS:

Defines rule #33.

Simplify [22] cadec=ddeb.

Reduce RHS:

Defines rule #36.

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

Overlap of [27] addec=aeeb with [51] ddec=bee:

Critical pair: abee=aeeb.

Flip LHS and RHS.

Defines rule #22.

Referenced by [64].

Overlap of [29] cddec=ceeb with [51] ddec=bee:

Critical pair: cbee=ceeb.

Flip LHS and RHS.

Defines rule #19.

Referenced by [62].

Overlap of [30] dddec=deeb with [51] ddec=bee:

Critical pair: dbee=deeb.

Flip LHS and RHS.

Defines rule #28.

Overlap of [37] aaddeb=ecdec with [47] ddeb=bead:

Critical pair: aabead=ecdec.

Defines rule #50.

Referenced by [72], [73].

Overlap of [59] ceeb=cbee with [2] ba=c:

Critical pair: ceec=cbeea.

Reduce RHS:

Defines rule #18.

Referenced by [63].

Overlap of [6] aac=eb with [62] ceec=ccee:

Critical pair: aaccee=ebeec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #45.

Overlap of [58] aeeb=abee with [2] ba=c:

Critical pair: aeec=abeea.

Reduce RHS:

Defines rule #21.

Referenced by [65].

Overlap of [3] caa=d with [64] aeec=acee:

Critical pair: caacee=deec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Overlap of [16] beac=cdeb with [57] cadec=bead:

Critical pair: beabead=cdebadec.

Reduce RHS:

Defines rule #60.

Overlap of [17] dca=cec with [57] cadec=bead:

Critical pair: dbead=cecdec.

Flip LHS and RHS.

Defines rule #48.

Overlap of [18] caca=bec with [57] cadec=bead:

Critical pair: cabead=becdec.

Flip LHS and RHS.

Defines rule #52.

Overlap of [35] daca=caec with [57] cadec=bead:

Critical pair: dabead=caecdec.

Flip LHS and RHS.

Defines rule #56.

Overlap of [36] eaca=adec with [57] cadec=bead:

Critical pair: eabead=adecdec.

Flip LHS and RHS.

Defines rule #58.

Overlap of [55] ebdec=ecdeb with [23] ecec=aaad:

Critical pair: ebdaaad=ecdebec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #61.

Overlap of [61] aabead=ecdec with [17] dca=cec:

Critical pair: aabeacec=ecdecca.

Reduce LHS:

Defines rule #62.

Overlap of [61] aabead=ecdec with [51] ddec=bee:

Critical pair: aabeabee=ecdecdec.

Flip LHS and RHS.

Defines rule #63.