| Back: | ⟨a, b | abaabbbbaab=1⟩ |
|---|
Completion settings:
Axiom: abaabbbbaab=1.
Referenced by [4].
Axiom: aa=c.
Defines rule #5.
Referenced by [3], [4], [5], [7], [10], [24], [26], [40], [47], [50], [54], [57], [59], [61], [62], [64].
Axiom: bbbbaabab=d.
Reduce LHS:
| [2] | bbbb(aa)bab |
| ⇒ bbbbcbab |
Defines rule #19.
Referenced by [6], [8], [9], [17], [18], [25], [29], [42], [54].
Overlap of [1] abaabbbbaab=1 with [2] aa=c:
Critical pair: abcbbbbaab=1.
Reduce LHS:
| [2] | abcbbbb(aa)b |
| ⇒ abcbbbbcb |
Referenced by [7], [8], [9], [11], [13], [16], [19].
Overlap of [2] aa=c with [2] aa=c:
Critical pair: ac=ca.
Defines rule #3.
Referenced by [12], [23], [30], [51], [56], [63], [66].
Overlap of [3] bbbbcbab=d with [3] bbbbcbab=d:
Critical pair: bbbbcbad=dbbbcbab.
Flip LHS and RHS.
Referenced by [28].
Overlap of [2] aa=c with [4] abcbbbbcb=1:
Critical pair: a=cbcbbbbcb.
Flip LHS and RHS.
Referenced by [13].
Overlap of [4] abcbbbbcb=1 with [3] bbbbcbab=d:
Critical pair: abcd=ab.
Referenced by [10].
Overlap of [4] abcbbbbcb=1 with [3] bbbbcbab=d:
Critical pair: abcbbbbcd=bbbcbab.
Referenced by [14].
Overlap of [2] aa=c with [8] abcd=ab:
Critical pair: aab=cbcd.
Reduce LHS:
| [2] | (aa)b |
| ⇒ cb |
Flip LHS and RHS.
Referenced by [11].
Overlap of [4] abcbbbbcb=1 with [10] cbcd=cb:
Critical pair: abcbbbbcb=cd.
Reduce LHS:
| [4] | (abcbbbbcb) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #1.
Referenced by [12], [14], [27], [33], [37], [41], [49], [55], [65].
Overlap of [5] ac=ca with [11] cd=1:
Critical pair: a=cad.
Flip LHS and RHS.
Referenced by [21].
Overlap of [4] abcbbbbcb=1 with [7] cbcbbbbcb=a:
Critical pair: abcbbbba=cbbbbcb.
Referenced by [15].
Overlap of [9] abcbbbbcd=bbbcbab with [11] cd=1:
Critical pair: abcbbbb=bbbcbab.
Referenced by [15], [16], [17], [19].
Overlap of [13] abcbbbba=cbbbbcb with [14] abcbbbb=bbbcbab:
Critical pair: bbbcbaba=cbbbbcb.
Flip LHS and RHS.
Defines rule #14.
Overlap of [4] abcbbbbcb=1 with [14] abcbbbb=bbbcbab:
Critical pair: bbbcbabcb=1.
Referenced by [18], [19], [20].
Overlap of [14] abcbbbb=bbbcbab with [3] bbbbcbab=d:
Critical pair: abcbbbd=bbbcbabbbbcbab.
Reduce RHS:
| [3] | bbbcba(bbbbcbab) |
| ⇒ bbbcbad |
Referenced by [22].
Overlap of [3] bbbbcbab=d with [16] bbbcbabcb=1:
Critical pair: b=dcb.
Flip LHS and RHS.
Referenced by [20].
Overlap of [4] abcbbbbcb=1 with [16] bbbcbabcb=1:
Critical pair: abcbbbbc=bbcbabcb.
Reduce LHS:
| [14] | (abcbbbb)c |
| ⇒ bbbcbabc |
Flip LHS and RHS.
Referenced by [29].
Overlap of [18] dcb=b with [16] bbbcbabcb=1:
Critical pair: dc=bbbcbabcb.
Reduce RHS:
| [16] | (bbbcbabcb) |
| ⇒ 1 |
Defines rule #2.
Referenced by [21], [23], [29], [31], [40], [47], [50], [54], [57], [59], [61], [62].
Overlap of [20] dc=1 with [12] cad=a:
Critical pair: da=ad.
Flip LHS and RHS.
Defines rule #4.
Referenced by [22], [27], [28], [35], [38], [41], [58], [60], [65].
Simplify [17] abcbbbd=bbbcbad.
Reduce RHS:
| [21] | bbbcb(ad) |
| ⇒ bbbcbda |
Referenced by [23].
Overlap of [22] abcbbbd=bbbcbda with [20] dc=1:
Critical pair: abcbbb=bbbcbdac.
Reduce RHS:
| [5] | bbbcbd(ac) |
| [20] | ⇒ bbbcb(dc)a |
| ⇒ bbbcba |
Defines rule #12.
Overlap of [2] aa=c with [23] abcbbb=bbbcba:
Critical pair: abbbcba=cbcbbb.
Overlap of [3] bbbbcbab=d with [24] abbbcba=cbcbbb:
Critical pair: bbbbcbcbcbbb=dbbcba.
Defines rule #33.
Overlap of [24] abbbcba=cbcbbb with [2] aa=c:
Critical pair: abbbcbc=cbcbbba.
Referenced by [27].
Overlap of [26] abbbcbc=cbcbbba with [11] cd=1:
Critical pair: abbbcb=cbcbbbad.
Reduce RHS:
| [21] | cbcbbb(ad) |
| ⇒ cbcbbbda |
Defines rule #11.
Referenced by [36], [39], [40], [48], [50], [52], [54].
Simplify [6] dbbbcbab=bbbbcbad.
Reduce RHS:
| [21] | bbbbcb(ad) |
| ⇒ bbbbcbda |
Defines rule #16.
Referenced by [48].
Overlap of [19] bbcbabcb=bbbcbabc with [19] bbcbabcb=bbbcbabc:
Critical pair: bbcbabcbbbcbabc=bbbcbabcbcbabcb.
Reduce LHS:
| [19] | (bbcbabcb)bbcbabc |
| [19] | ⇒ b(bbcbabcb)bcbabc |
| [3] | ⇒ (bbbbcbab)cbcbabc |
| [20] | ⇒ (dc)bcbabc |
| ⇒ bcbabc |
Reduce RHS:
| [19] | b(bbcbabcb)cbabcb |
| [3] | ⇒ (bbbbcbab)ccbabcb |
| [20] | ⇒ (dc)cbabcb |
| ⇒ cbabcb |
Flip LHS and RHS.
Defines rule #6.
Referenced by [30], [31], [32], [34], [40], [50].
Overlap of [5] ac=ca with [29] cbabcb=bcbabc:
Critical pair: abcbabc=cababcb.
Flip LHS and RHS.
Defines rule #8.
Overlap of [20] dc=1 with [29] cbabcb=bcbabc:
Critical pair: dbcbabc=babcb.
Overlap of [29] cbabcb=bcbabc with [29] cbabcb=bcbabc:
Critical pair: cbabbcbabc=bcbabcabcb.
Overlap of [31] dbcbabc=babcb with [11] cd=1:
Critical pair: dbcbab=babcbd.
Defines rule #7.
Referenced by [35], [36], [43].
Overlap of [31] dbcbabc=babcb with [29] cbabcb=bcbabc:
Critical pair: dbbcbabc=babcbb.
Referenced by [37].
Overlap of [21] ad=da with [33] dbcbab=babcbd:
Critical pair: ababcbd=dabcbab.
Flip LHS and RHS.
Defines rule #9.
Referenced by [44].
Overlap of [33] dbcbab=babcbd with [27] abbbcb=cbcbbbda:
Critical pair: dbcbcbcbbbda=babcbdbbcb.
Referenced by [57].
Overlap of [34] dbbcbabc=babcbb with [11] cd=1:
Critical pair: dbbcbab=babcbbd.
Defines rule #10.
Referenced by [38], [39], [45].
Overlap of [21] ad=da with [37] dbbcbab=babcbbd:
Critical pair: ababcbbd=dabbcbab.
Flip LHS and RHS.
Defines rule #13.
Overlap of [37] dbbcbab=babcbbd with [27] abbbcb=cbcbbbda:
Critical pair: dbbcbcbcbbbda=babcbbdbbcb.
Referenced by [59].
Overlap of [38] dabbcbab=ababcbbd with [29] cbabcb=bcbabc:
Critical pair: dabbbcbabc=ababcbbdcb.
Reduce LHS:
| [27] | d(abbbcb)abc |
| [20] | ⇒ (dc)bcbbbdaabc |
| [2] | ⇒ bcbbbd(aa)bc |
| [20] | ⇒ bcbbb(dc)bc |
| ⇒ bcbbbbc |
Reduce RHS:
| [20] | ababcbb(dc)b |
| [23] | ⇒ ab(abcbbb) |
| ⇒ abbbbcba |
Flip LHS and RHS.
Referenced by [41].
Overlap of [40] abbbbcba=bcbbbbc with [21] ad=da:
Critical pair: abbbbcbda=bcbbbbcd.
Reduce RHS:
| [11] | bcbbbb(cd) |
| ⇒ bcbbbb |
Referenced by [42], [43], [44], [45], [46], [47].
Overlap of [3] bbbbcbab=d with [41] abbbbcbda=bcbbbb:
Critical pair: bbbbcbbcbbbb=dbbbcbda.
Defines rule #37.
Referenced by [54].
Overlap of [33] dbcbab=babcbd with [41] abbbbcbda=bcbbbb:
Critical pair: dbcbbcbbbb=babcbdbbbcbda.
Defines rule #25.
Overlap of [35] dabcbab=ababcbd with [41] abbbbcbda=bcbbbb:
Critical pair: dabcbbcbbbb=ababcbdbbbcbda.
Defines rule #27.
Overlap of [37] dbbcbab=babcbbd with [41] abbbbcbda=bcbbbb:
Critical pair: dbbcbbcbbbb=babcbbdbbbcbda.
Defines rule #30.
Overlap of [38] dabbcbab=ababcbbd with [41] abbbbcbda=bcbbbb:
Critical pair: dabbcbbcbbbb=ababcbbdbbbcbda.
Defines rule #32.
Overlap of [41] abbbbcbda=bcbbbb with [2] aa=c:
Critical pair: abbbbcbdc=bcbbbba.
Reduce LHS:
| [20] | abbbbcb(dc) |
| ⇒ abbbbcb |
Defines rule #17.
Referenced by [53].
Overlap of [28] dbbbcbab=bbbbcbda with [27] abbbcb=cbcbbbda:
Critical pair: dbbbcbcbcbbbda=bbbbcbdabbcb.
Referenced by [61].
Overlap of [32] cbabbcbabc=bcbabcabcb with [11] cd=1:
Critical pair: cbabbcbab=bcbabcabcbd.
Defines rule #15.
Referenced by [51], [52], [53].
Overlap of [32] cbabbcbabc=bcbabcabcb with [29] cbabcb=bcbabc:
Critical pair: cbabbbcbabc=bcbabcabcbb.
Reduce LHS:
| [27] | cb(abbbcb)abc |
| [2] | ⇒ cbcbcbbbd(aa)bc |
| [20] | ⇒ cbcbcbbb(dc)bc |
| ⇒ cbcbcbbbbc |
Referenced by [55].
Overlap of [5] ac=ca with [49] cbabbcbab=bcbabcabcbd:
Critical pair: abcbabcabcbd=cababbcbab.
Flip LHS and RHS.
Defines rule #18.
Overlap of [49] cbabbcbab=bcbabcabcbd with [27] abbbcb=cbcbbbda:
Critical pair: cbabbcbcbcbbbda=bcbabcabcbdbbcb.
Referenced by [62].
Overlap of [49] cbabbcbab=bcbabcabcbd with [47] abbbbcb=bcbbbba:
Critical pair: cbabbcbbcbbbba=bcbabcabcbdbbbcb.
Referenced by [64].
Overlap of [42] bbbbcbbcbbbb=dbbbcbda with [3] bbbbcbab=d:
Critical pair: bbbbcbbcbbbd=dbbbcbdabbbcbab.
Reduce RHS:
| [27] | dbbbcbd(abbbcb)ab |
| [20] | ⇒ dbbbcb(dc)bcbbbdaab |
| [2] | ⇒ dbbbcbbcbbbd(aa)b |
| [20] | ⇒ dbbbcbbcbbb(dc)b |
| ⇒ dbbbcbbcbbbb |
Flip LHS and RHS.
Defines rule #35.
Overlap of [50] cbcbcbbbbc=bcbabcabcbb with [11] cd=1:
Critical pair: cbcbcbbbb=bcbabcabcbbd.
Defines rule #20.
Referenced by [56].
Overlap of [5] ac=ca with [55] cbcbcbbbb=bcbabcabcbbd:
Critical pair: abcbabcabcbbd=cabcbcbbbb.
Flip LHS and RHS.
Defines rule #22.
Overlap of [36] dbcbcbcbbbda=babcbdbbcb with [2] aa=c:
Critical pair: dbcbcbcbbbdc=babcbdbbcba.
Reduce LHS:
| [20] | dbcbcbcbbb(dc) |
| ⇒ dbcbcbcbbb |
Defines rule #21.
Referenced by [58].
Overlap of [21] ad=da with [57] dbcbcbcbbb=babcbdbbcba:
Critical pair: ababcbdbbcba=dabcbcbcbbb.
Flip LHS and RHS.
Defines rule #23.
Overlap of [39] dbbcbcbcbbbda=babcbbdbbcb with [2] aa=c:
Critical pair: dbbcbcbcbbbdc=babcbbdbbcba.
Reduce LHS:
| [20] | dbbcbcbcbbb(dc) |
| ⇒ dbbcbcbcbbb |
Defines rule #24.
Referenced by [60].
Overlap of [21] ad=da with [59] dbbcbcbcbbb=babcbbdbbcba:
Critical pair: ababcbbdbbcba=dabbcbcbcbbb.
Flip LHS and RHS.
Defines rule #26.
Overlap of [48] dbbbcbcbcbbbda=bbbbcbdabbcb with [2] aa=c:
Critical pair: dbbbcbcbcbbbdc=bbbbcbdabbcba.
Reduce LHS:
| [20] | dbbbcbcbcbbb(dc) |
| ⇒ dbbbcbcbcbbb |
Defines rule #29.
Overlap of [52] cbabbcbcbcbbbda=bcbabcabcbdbbcb with [2] aa=c:
Critical pair: cbabbcbcbcbbbdc=bcbabcabcbdbbcba.
Reduce LHS:
| [20] | cbabbcbcbcbbb(dc) |
| ⇒ cbabbcbcbcbbb |
Defines rule #28.
Referenced by [63].
Overlap of [5] ac=ca with [62] cbabbcbcbcbbb=bcbabcabcbdbbcba:
Critical pair: abcbabcabcbdbbcba=cababbcbcbcbbb.
Flip LHS and RHS.
Defines rule #31.
Overlap of [53] cbabbcbbcbbbba=bcbabcabcbdbbbcb with [2] aa=c:
Critical pair: cbabbcbbcbbbbc=bcbabcabcbdbbbcba.
Referenced by [65].
Overlap of [64] cbabbcbbcbbbbc=bcbabcabcbdbbbcba with [11] cd=1:
Critical pair: cbabbcbbcbbbb=bcbabcabcbdbbbcbad.
Reduce RHS:
| [21] | bcbabcabcbdbbbcb(ad) |
| ⇒ bcbabcabcbdbbbcbda |
Defines rule #34.
Referenced by [66].
Overlap of [5] ac=ca with [65] cbabbcbbcbbbb=bcbabcabcbdbbbcbda:
Critical pair: abcbabcabcbdbbbcbda=cababbcbbcbbbb.
Flip LHS and RHS.
Defines rule #36.