| Back: | ⟨a, b | abaab=aaaba⟩ |
|---|
Completion settings:
Axiom: abaab=aaaba.
Referenced by [5].
Axiom: aa=c.
Defines rule #1.
Referenced by [5], [6], [7], [10], [18], [39].
Axiom: bc=d.
Defines rule #2.
Referenced by [6], [8], [9], [10], [11], [20], [24], [25], [29], [33].
Axiom: cba=e.
Defines rule #20.
Referenced by [9], [10], [12], [17], [19], [37].
Simplify [1] abaab=aaaba.
Reduce RHS:
| [2] | (aa)aba |
| ⇒ caba |
Referenced by [6].
Overlap of [5] abaab=caba with [2] aa=c:
Critical pair: abcb=caba.
Reduce LHS:
| [3] | a(bc)b |
| ⇒ adb |
Flip LHS and RHS.
Referenced by [17].
Overlap of [2] aa=c with [2] aa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #3.
Referenced by [8], [17], [38], [42], [44], [79].
Overlap of [3] bc=d with [7] ca=ac:
Critical pair: bac=da.
Defines rule #16.
Referenced by [12], [13], [14], [16], [26].
Overlap of [3] bc=d with [4] cba=e:
Critical pair: be=dba.
Flip LHS and RHS.
Defines rule #10.
Referenced by [14], [21], [30], [34], [61], [68].
Overlap of [4] cba=e with [2] aa=c:
Critical pair: cbc=ea.
Reduce LHS:
| [3] | c(bc) |
| ⇒ cd |
Defines rule #4.
Referenced by [11], [13], [15], [18], [79].
Overlap of [3] bc=d with [10] cd=ea:
Critical pair: bea=dd.
Defines rule #17.
Referenced by [22], [24], [27], [31], [35], [40].
Overlap of [8] bac=da with [4] cba=e:
Critical pair: bae=daba.
Flip LHS and RHS.
Defines rule #26.
Overlap of [8] bac=da with [10] cd=ea:
Critical pair: baea=dad.
Defines rule #37.
Referenced by [57], [58], [59], [60], [62], [63], [67], [73].
Overlap of [9] dba=be with [8] bac=da:
Critical pair: dda=bec.
Flip LHS and RHS.
Defines rule #18.
Referenced by [15], [23], [28], [32], [36].
Overlap of [14] bec=dda with [10] cd=ea:
Critical pair: beea=ddad.
Defines rule #38.
Referenced by [61].
Overlap of [12] daba=bae with [8] bac=da:
Critical pair: dada=baec.
Flip LHS and RHS.
Referenced by [45].
Overlap of [6] caba=adb with [7] ca=ac:
Critical pair: acba=adb.
Reduce LHS:
| [4] | a(cba) |
| ⇒ ae |
Flip LHS and RHS.
Defines rule #5.
Referenced by [18], [19], [20], [21], [22], [23], [57].
Overlap of [2] aa=c with [17] adb=ae:
Critical pair: aae=cdb.
Reduce LHS:
| [2] | (aa)e |
| ⇒ ce |
Reduce RHS:
| [10] | (cd)b |
| ⇒ eab |
Flip LHS and RHS.
Defines rule #12.
Referenced by [24], [25], [26], [27], [28], [41], [49], [50], [53], [55], [58].
Overlap of [4] cba=e with [17] adb=ae:
Critical pair: cbae=edb.
Reduce LHS:
| [4] | (cba)e |
| ⇒ ee |
Flip LHS and RHS.
Defines rule #13.
Referenced by [33], [34], [35], [36], [43], [59].
Overlap of [17] adb=ae with [3] bc=d:
Critical pair: add=aec.
Flip LHS and RHS.
Defines rule #6.
Referenced by [37], [38], [45].
Overlap of [17] adb=ae with [9] dba=be:
Critical pair: abe=aea.
Defines rule #7.
Referenced by [39], [40], [41].
Overlap of [17] adb=ae with [11] bea=dd:
Critical pair: addd=aeea.
Flip LHS and RHS.
Defines rule #24.
Referenced by [64].
Overlap of [17] adb=ae with [14] bec=dda:
Critical pair: addda=aeec.
Referenced by [46].
Overlap of [11] bea=dd with [18] eab=ce:
Critical pair: bce=ddb.
Reduce LHS:
| [3] | (bc)e |
| ⇒ de |
Flip LHS and RHS.
Defines rule #8.
Referenced by [29], [30], [31], [32], [37], [40], [60], [70].
Overlap of [18] eab=ce with [3] bc=d:
Critical pair: ead=cec.
Flip LHS and RHS.
Defines rule #19.
Overlap of [18] eab=ce with [8] bac=da:
Critical pair: eada=ceac.
Flip LHS and RHS.
Defines rule #39.
Referenced by [81].
Overlap of [18] eab=ce with [11] bea=dd:
Critical pair: eadd=ceea.
Flip LHS and RHS.
Defines rule #40.
Referenced by [72].
Overlap of [18] eab=ce with [14] bec=dda:
Critical pair: eadda=ceec.
Referenced by [47].
Overlap of [24] ddb=de with [3] bc=d:
Critical pair: ddd=dec.
Flip LHS and RHS.
Defines rule #9.
Referenced by [42].
Overlap of [24] ddb=de with [9] dba=be:
Critical pair: dbe=dea.
Defines rule #11.
Referenced by [43].
Overlap of [24] ddb=de with [11] bea=dd:
Critical pair: dddd=deea.
Flip LHS and RHS.
Defines rule #29.
Referenced by [65].
Overlap of [24] ddb=de with [14] bec=dda:
Critical pair: dddda=deec.
Referenced by [48].
Overlap of [19] edb=ee with [3] bc=d:
Critical pair: edd=eec.
Flip LHS and RHS.
Defines rule #14.
Referenced by [36], [44], [46], [47], [48], [74], [75], [77], [78], [80], [82], [83], [84], [86].
Overlap of [19] edb=ee with [9] dba=be:
Critical pair: ebe=eea.
Defines rule #15.
Overlap of [19] edb=ee with [11] bea=dd:
Critical pair: eddd=eeea.
Flip LHS and RHS.
Defines rule #34.
Referenced by [51], [52], [54], [56], [66].
Overlap of [19] edb=ee with [14] bec=dda:
Critical pair: eddda=eeec.
Reduce RHS:
| [33] | e(eec) |
| ⇒ eedd |
Defines rule #55.
Referenced by [78].
Overlap of [20] aec=add with [4] cba=e:
Critical pair: aee=addba.
Reduce RHS:
| [24] | a(ddb)a |
| ⇒ adea |
Flip LHS and RHS.
Defines rule #22.
Referenced by [49], [51], [82], [88].
Overlap of [20] aec=add with [7] ca=ac:
Critical pair: aeac=adda.
Defines rule #23.
Referenced by [61], [74], [75], [77], [78], [79], [80].
Overlap of [2] aa=c with [21] abe=aea:
Critical pair: aaea=cbe.
Reduce LHS:
| [2] | (aa)ea |
| ⇒ cea |
Flip LHS and RHS.
Defines rule #21.
Overlap of [11] bea=dd with [21] abe=aea:
Critical pair: beaea=ddbe.
Reduce LHS:
| [11] | (bea)ea |
| ⇒ ddea |
Reduce RHS:
| [24] | (ddb)e |
| ⇒ dee |
Defines rule #27.
Referenced by [50], [52], [71], [74], [75], [77], [78], [80], [83], [89].
Overlap of [18] eab=ce with [21] abe=aea:
Critical pair: eaea=cee.
Defines rule #31.
Referenced by [51], [52], [53], [54], [56], [57], [58], [59], [60], [62], [63], [67], [73], [84], [90].
Overlap of [29] dec=ddd with [7] ca=ac:
Critical pair: deac=ddda.
Defines rule #28.
Referenced by [85].
Overlap of [19] edb=ee with [30] dbe=dea:
Critical pair: edea=eee.
Defines rule #32.
Referenced by [55], [56], [86], [91].
Overlap of [33] eec=edd with [7] ca=ac:
Critical pair: eeac=edda.
Defines rule #33.
Referenced by [64], [65], [66], [72], [87].
Overlap of [16] baec=dada with [20] aec=add:
Critical pair: badd=dada.
Defines rule #36.
Referenced by [68], [69], [70], [71], [76], [80].
Simplify [23] addda=aeec.
Reduce RHS:
| [33] | a(eec) |
| ⇒ aedd |
Defines rule #43.
Referenced by [74].
Simplify [28] eadda=ceec.
Reduce RHS:
| [33] | c(eec) |
| ⇒ cedd |
Defines rule #53.
Referenced by [77].
Simplify [32] dddda=deec.
Reduce RHS:
| [33] | d(eec) |
| ⇒ dedd |
Defines rule #49.
Overlap of [37] adea=aee with [18] eab=ce:
Critical pair: adce=aeeb.
Flip LHS and RHS.
Defines rule #25.
Referenced by [62].
Overlap of [40] ddea=dee with [18] eab=ce:
Critical pair: ddce=deeb.
Flip LHS and RHS.
Defines rule #30.
Referenced by [63].
Overlap of [37] adea=aee with [41] eaea=cee:
Critical pair: adcee=aeeea.
Reduce RHS:
| [35] | a(eeea) |
| ⇒ aeddd |
Flip LHS and RHS.
Defines rule #45.
Referenced by [74].
Overlap of [40] ddea=dee with [41] eaea=cee:
Critical pair: ddcee=deeea.
Reduce RHS:
| [35] | d(eeea) |
| ⇒ deddd |
Flip LHS and RHS.
Defines rule #51.
Overlap of [41] eaea=cee with [18] eab=ce:
Critical pair: eace=ceeb.
Flip LHS and RHS.
Defines rule #41.
Referenced by [73].
Overlap of [41] eaea=cee with [41] eaea=cee:
Critical pair: eacee=ceeea.
Reduce RHS:
| [35] | c(eeea) |
| ⇒ ceddd |
Flip LHS and RHS.
Defines rule #60.
Referenced by [77].
Overlap of [43] edea=eee with [18] eab=ce:
Critical pair: edce=eeeb.
Flip LHS and RHS.
Defines rule #35.
Referenced by [67].
Overlap of [43] edea=eee with [41] eaea=cee:
Critical pair: edcee=eeeea.
Reduce RHS:
| [35] | e(eeea) |
| ⇒ eeddd |
Flip LHS and RHS.
Defines rule #57.
Referenced by [78].
Overlap of [17] adb=ae with [13] baea=dad:
Critical pair: addad=aeaea.
Reduce RHS:
| [41] | a(eaea) |
| ⇒ acee |
Defines rule #42.
Overlap of [18] eab=ce with [13] baea=dad:
Critical pair: eadad=ceaea.
Reduce RHS:
| [41] | c(eaea) |
| ⇒ ccee |
Defines rule #52.
Overlap of [19] edb=ee with [13] baea=dad:
Critical pair: eddad=eeaea.
Reduce RHS:
| [41] | e(eaea) |
| ⇒ ecee |
Defines rule #54.
Overlap of [24] ddb=de with [13] baea=dad:
Critical pair: dddad=deaea.
Reduce RHS:
| [41] | d(eaea) |
| ⇒ dcee |
Defines rule #48.
Overlap of [9] dba=be with [38] aeac=adda:
Critical pair: dbadda=beeac.
Reduce LHS:
| [9] | (dba)dda |
| ⇒ bedda |
Reduce RHS:
| [15] | (beea)c |
| ⇒ ddadc |
Defines rule #58.
Overlap of [49] aeeb=adce with [13] baea=dad:
Critical pair: aeedad=adceaea.
Reduce RHS:
| [41] | adc(eaea) |
| ⇒ adccee |
Defines rule #61.
Overlap of [50] deeb=ddce with [13] baea=dad:
Critical pair: deedad=ddceaea.
Reduce RHS:
| [41] | ddc(eaea) |
| ⇒ ddccee |
Defines rule #64.
Overlap of [22] aeea=addd with [44] eeac=edda:
Critical pair: aedda=adddc.
Defines rule #44.
Overlap of [31] deea=dddd with [44] eeac=edda:
Critical pair: dedda=ddddc.
Defines rule #50.
Overlap of [35] eeea=eddd with [44] eeac=edda:
Critical pair: eedda=edddc.
Defines rule #56.
Overlap of [55] eeeb=edce with [13] baea=dad:
Critical pair: eeedad=edceaea.
Reduce RHS:
| [41] | edc(eaea) |
| ⇒ edccee |
Defines rule #65.
Overlap of [9] dba=be with [45] badd=dada:
Critical pair: ddada=bedd.
Defines rule #47.
Overlap of [12] daba=bae with [45] badd=dada:
Critical pair: dadada=baedd.
Defines rule #62.
Overlap of [45] badd=dada with [24] ddb=de:
Critical pair: bade=dadab.
Flip LHS and RHS.
Defines rule #46.
Overlap of [45] badd=dada with [40] ddea=dee:
Critical pair: badee=dadaea.
Flip LHS and RHS.
Defines rule #63.
Overlap of [27] ceea=eadd with [44] eeac=edda:
Critical pair: cedda=eaddc.
Defines rule #59.
Overlap of [53] ceeb=eace with [13] baea=dad:
Critical pair: ceedad=eaceaea.
Reduce RHS:
| [41] | eac(eaea) |
| ⇒ eaccee |
Defines rule #66.
Overlap of [46] addda=aedd with [38] aeac=adda:
Critical pair: adddadda=aeddeac.
Reduce LHS:
| [46] | (addda)dda |
| [51] | ⇒ (aeddd)da |
| ⇒ adceeda |
Reduce RHS:
| [40] | ae(ddea)c |
| [33] | ⇒ aed(eec) |
| ⇒ aededd |
Defines rule #67.
Referenced by [79].
Overlap of [48] dddda=dedd with [38] aeac=adda:
Critical pair: ddddadda=deddeac.
Reduce LHS:
| [48] | (dddda)dda |
| [52] | ⇒ (deddd)da |
| ⇒ ddceeda |
Reduce RHS:
| [40] | de(ddea)c |
| [33] | ⇒ ded(eec) |
| ⇒ dededd |
Defines rule #69.
Overlap of [45] badd=dada with [48] dddda=dedd:
Critical pair: badedd=dadadda.
Flip LHS and RHS.
Defines rule #68.
Referenced by [80].
Overlap of [47] eadda=cedd with [38] aeac=adda:
Critical pair: eaddadda=ceddeac.
Reduce LHS:
| [47] | (eadda)dda |
| [54] | ⇒ (ceddd)da |
| ⇒ eaceeda |
Reduce RHS:
| [40] | ce(ddea)c |
| [33] | ⇒ ced(eec) |
| ⇒ cededd |
Defines rule #70.
Referenced by [81], [82], [83], [84], [85], [86], [87].
Overlap of [36] eddda=eedd with [38] aeac=adda:
Critical pair: edddadda=eeddeac.
Reduce LHS:
| [36] | (eddda)dda |
| [56] | ⇒ (eeddd)da |
| ⇒ edceeda |
Reduce RHS:
| [40] | ee(ddea)c |
| [33] | ⇒ eed(eec) |
| ⇒ eededd |
Defines rule #71.
Overlap of [7] ca=ac with [74] adceeda=aededd:
Critical pair: caededd=acdceeda.
Reduce LHS:
| [7] | (ca)ededd |
| ⇒ acededd |
Reduce RHS:
| [10] | a(cd)ceeda |
| [38] | ⇒ (aeac)eeda |
| ⇒ addaeeda |
Flip LHS and RHS.
Defines rule #72.
Overlap of [76] dadadda=badedd with [38] aeac=adda:
Critical pair: dadaddadda=badeddeac.
Reduce LHS:
| [76] | (dadadda)dda |
| [52] | ⇒ ba(deddd)da |
| [45] | ⇒ (badd)ceeda |
| ⇒ dadaceeda |
Reduce RHS:
| [40] | bade(ddea)c |
| [33] | ⇒ baded(eec) |
| ⇒ badededd |
Defines rule #81.
Overlap of [26] ceac=eada with [77] eaceeda=cededd:
Critical pair: ccededd=eadaeeda.
Flip LHS and RHS.
Defines rule #76.
Referenced by [88], [89], [90], [91].
Overlap of [37] adea=aee with [77] eaceeda=cededd:
Critical pair: adcededd=aeeceeda.
Reduce RHS:
| [33] | a(eec)eeda |
| ⇒ aeddeeda |
Flip LHS and RHS.
Defines rule #73.
Overlap of [40] ddea=dee with [77] eaceeda=cededd:
Critical pair: ddcededd=deeceeda.
Reduce RHS:
| [33] | d(eec)eeda |
| ⇒ deddeeda |
Flip LHS and RHS.
Defines rule #75.
Overlap of [41] eaea=cee with [77] eaceeda=cededd:
Critical pair: eacededd=ceeceeda.
Reduce RHS:
| [33] | c(eec)eeda |
| ⇒ ceddeeda |
Flip LHS and RHS.
Defines rule #79.
Overlap of [42] deac=ddda with [77] eaceeda=cededd:
Critical pair: dcededd=dddaeeda.
Flip LHS and RHS.
Defines rule #74.
Overlap of [43] edea=eee with [77] eaceeda=cededd:
Critical pair: edcededd=eeeceeda.
Reduce RHS:
| [33] | e(eec)eeda |
| ⇒ eeddeeda |
Flip LHS and RHS.
Defines rule #78.
Overlap of [44] eeac=edda with [77] eaceeda=cededd:
Critical pair: ecededd=eddaeeda.
Flip LHS and RHS.
Defines rule #77.
Overlap of [37] adea=aee with [81] eadaeeda=ccededd:
Critical pair: adccededd=aeedaeeda.
Flip LHS and RHS.
Defines rule #80.
Overlap of [40] ddea=dee with [81] eadaeeda=ccededd:
Critical pair: ddccededd=deedaeeda.
Flip LHS and RHS.
Defines rule #82.
Overlap of [41] eaea=cee with [81] eadaeeda=ccededd:
Critical pair: eaccededd=ceedaeeda.
Flip LHS and RHS.
Defines rule #84.
Overlap of [43] edea=eee with [81] eadaeeda=ccededd:
Critical pair: edccededd=eeedaeeda.
Flip LHS and RHS.
Defines rule #83.