| Back: | ⟨a, b | ababaabbbba=1⟩ |
|---|
Completion settings:
Axiom: ababaabbbba=1.
Referenced by [4].
Axiom: aa=c.
Defines rule #5.
Referenced by [3], [4], [5], [7], [26], [36], [37], [40], [41], [46], [52], [55], [59], [61].
Axiom: bbbbaabab=d.
Reduce LHS:
| [2] | bbbb(aa)bab |
| ⇒ bbbbcbab |
Referenced by [6], [9], [12], [17], [18], [19].
Overlap of [1] ababaabbbba=1 with [2] aa=c:
Critical pair: ababcbbbba=1.
Referenced by [6], [7], [8], [10], [11], [13], [21].
Overlap of [2] aa=c with [2] aa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #3.
Referenced by [31], [34], [57], [60], [63].
Overlap of [3] bbbbcbab=d with [4] ababcbbbba=1:
Critical pair: bbbbcb=dabcbbbba.
Flip LHS and RHS.
Referenced by [39].
Overlap of [4] ababcbbbba=1 with [2] aa=c:
Critical pair: ababcbbbbc=a.
Referenced by [9], [10], [14].
Overlap of [4] ababcbbbba=1 with [4] ababcbbbba=1:
Critical pair: ababcbbbb=babcbbbba.
Flip LHS and RHS.
Referenced by [22].
Overlap of [3] bbbbcbab=d with [7] ababcbbbbc=a:
Critical pair: bbbbcba=dabcbbbbc.
Referenced by [24].
Overlap of [4] ababcbbbba=1 with [7] ababcbbbbc=a:
Critical pair: ababcbbbba=babcbbbbc.
Reduce LHS:
| [4] | (ababcbbbba) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [11], [12], [15], [16].
Overlap of [4] ababcbbbba=1 with [10] babcbbbbc=1:
Critical pair: ababcbbb=bcbbbbc.
Flip LHS and RHS.
Defines rule #14.
Referenced by [24].
Overlap of [10] babcbbbbc=1 with [3] bbbbcbab=d:
Critical pair: babcd=bab.
Referenced by [13].
Overlap of [4] ababcbbbba=1 with [12] babcd=bab:
Critical pair: ababcbbbbab=bcd.
Reduce LHS:
| [4] | (ababcbbbba)b |
| ⇒ b |
Flip LHS and RHS.
Referenced by [14], [15], [33], [34].
Overlap of [7] ababcbbbbc=a with [13] bcd=b:
Critical pair: ababcbbbb=ad.
Overlap of [10] babcbbbbc=1 with [13] bcd=b:
Critical pair: babcbbbb=d.
Defines rule #19.
Referenced by [16], [17], [18], [19], [20], [23], [35], [36], [47], [55].
Overlap of [10] babcbbbbc=1 with [15] babcbbbb=d:
Critical pair: dc=1.
Defines rule #1.
Referenced by [27], [38], [45], [56], [62].
Overlap of [15] babcbbbb=d with [3] bbbbcbab=d:
Critical pair: babcbd=dbcbab.
Defines rule #7.
Referenced by [27], [28], [42], [48].
Overlap of [15] babcbbbb=d with [3] bbbbcbab=d:
Critical pair: babcbbd=dbbcbab.
Defines rule #10.
Referenced by [34], [43], [49].
Overlap of [15] babcbbbb=d with [3] bbbbcbab=d:
Critical pair: babcbbbd=dbbbcbab.
Overlap of [15] babcbbbb=d with [15] babcbbbb=d:
Critical pair: babcbbbd=dabcbbbb.
Reduce LHS:
| [19] | (babcbbbd) |
| ⇒ dbbbcbab |
Referenced by [25].
Overlap of [4] ababcbbbba=1 with [14] ababcbbbb=ad:
Critical pair: ada=1.
Simplify [8] babcbbbba=ababcbbbb.
Reduce RHS:
| [14] | (ababcbbbb) |
| ⇒ ad |
Referenced by [23].
Overlap of [22] babcbbbba=ad with [15] babcbbbb=d:
Critical pair: da=ad.
Defines rule #4.
Referenced by [24], [25], [26], [28], [39], [45], [58], [62].
Simplify [9] bbbbcba=dabcbbbbc.
Reduce RHS:
| [23] | (da)bcbbbbc |
| [11] | ⇒ ad(bcbbbbc) |
| [21] | ⇒ (ada)babcbbb |
| ⇒ babcbbb |
Simplify [19] babcbbbd=dbbbcbab.
Reduce RHS:
| [20] | (dbbbcbab) |
| [23] | ⇒ (da)bcbbbb |
| ⇒ adbcbbbb |
Defines rule #16.
Simplify [21] ada=1.
Reduce LHS:
| [23] | a(da) |
| [2] | ⇒ (aa)d |
| ⇒ cd |
Defines rule #2.
Referenced by [29], [34], [46], [52], [55], [59].
Overlap of [17] babcbd=dbcbab with [16] dc=1:
Critical pair: babcb=dbcbabc.
Flip LHS and RHS.
Referenced by [29], [30], [32], [33].
Overlap of [17] babcbd=dbcbab with [23] da=ad:
Critical pair: babcbad=dbcbaba.
Defines rule #9.
Referenced by [33], [44], [50].
Overlap of [26] cd=1 with [27] dbcbabc=babcb:
Critical pair: cbabcb=bcbabc.
Flip LHS and RHS.
Defines rule #6.
Referenced by [30], [31], [34], [52].
Overlap of [27] dbcbabc=babcb with [29] bcbabc=cbabcb:
Critical pair: dbcbacbabcb=babcbbabc.
Flip LHS and RHS.
Defines rule #15.
Referenced by [52], [53], [54].
Overlap of [29] bcbabc=cbabcb with [5] ca=ac:
Critical pair: bcbabac=cbabcba.
Defines rule #8.
Referenced by [32].
Overlap of [27] dbcbabc=babcb with [31] bcbabac=cbabcba:
Critical pair: dbcbacbabcba=babcbbabac.
Flip LHS and RHS.
Defines rule #18.
Overlap of [27] dbcbabc=babcb with [28] babcbad=dbcbaba:
Critical pair: dbcdbcbaba=babcbbad.
Reduce LHS:
| [13] | d(bcd)bcbaba |
| ⇒ dbbcbaba |
Flip LHS and RHS.
Defines rule #13.
Referenced by [51].
Overlap of [29] bcbabc=cbabcb with [18] babcbbd=dbbcbab:
Critical pair: bcdbbcbab=cbabcbbbd.
Reduce LHS:
| [13] | (bcd)bbcbab |
| ⇒ bbbcbab |
Reduce RHS:
| [25] | c(babcbbbd) |
| [5] | ⇒ (ca)dbcbbbb |
| [26] | ⇒ a(cd)bcbbbb |
| ⇒ abcbbbb |
Referenced by [35], [36], [37].
Overlap of [34] bbbcbab=abcbbbb with [15] babcbbbb=d:
Critical pair: bbbcbad=abcbbbbabcbbbb.
Reduce RHS:
| [15] | abcbbb(babcbbbb) |
| ⇒ abcbbbd |
Overlap of [34] bbbcbab=abcbbbb with [34] bbbcbab=abcbbbb:
Critical pair: bbbcbaabcbbbb=abcbbbbbbcbab.
Reduce LHS:
| [2] | bbbcb(aa)bcbbbb |
| ⇒ bbbcbcbcbbbb |
Reduce RHS:
| [24] | abcbb(bbbbcba)b |
| [15] | ⇒ abcbb(babcbbbb) |
| ⇒ abcbbd |
Defines rule #33.
Overlap of [34] bbbcbab=abcbbbb with [35] bbbcbad=abcbbbd:
Critical pair: bbbcbaabcbbbd=abcbbbbbbcbad.
Reduce LHS:
| [2] | bbbcb(aa)bcbbbd |
| ⇒ bbbcbcbcbbbd |
Reduce RHS:
| [24] | abcbb(bbbbcba)d |
| [25] | ⇒ abcbb(babcbbbd) |
| ⇒ abcbbadbcbbbb |
Defines rule #29.
Overlap of [35] bbbcbad=abcbbbd with [16] dc=1:
Critical pair: bbbcba=abcbbbdc.
Reduce RHS:
| [16] | abcbbb(dc) |
| ⇒ abcbbb |
Defines rule #12.
Referenced by [40].
Overlap of [6] dabcbbbba=bbbbcb with [23] da=ad:
Critical pair: adbcbbbba=bbbbcb.
Referenced by [46], [47], [48], [49], [50].
Overlap of [38] bbbcba=abcbbb with [2] aa=c:
Critical pair: bbbcbc=abcbbba.
Flip LHS and RHS.
Referenced by [41], [42], [43], [44], [51].
Overlap of [2] aa=c with [40] abcbbba=bbbcbc:
Critical pair: abbbcbc=cbcbbba.
Flip LHS and RHS.
Referenced by [45].
Overlap of [40] abcbbba=bbbcbc with [17] babcbd=dbcbab:
Critical pair: abcbbdbcbab=bbbcbcbcbd.
Flip LHS and RHS.
Defines rule #21.
Overlap of [40] abcbbba=bbbcbc with [18] babcbbd=dbbcbab:
Critical pair: abcbbdbbcbab=bbbcbcbcbbd.
Flip LHS and RHS.
Defines rule #24.
Overlap of [40] abcbbba=bbbcbc with [28] babcbad=dbcbaba:
Critical pair: abcbbdbcbaba=bbbcbcbcbad.
Flip LHS and RHS.
Defines rule #23.
Overlap of [16] dc=1 with [41] cbcbbba=abbbcbc:
Critical pair: dabbbcbc=bcbbba.
Reduce LHS:
| [23] | (da)bbbcbc |
| ⇒ adbbbcbc |
Flip LHS and RHS.
Defines rule #11.
Referenced by [52], [53], [55].
Overlap of [2] aa=c with [39] adbcbbbba=bbbbcb:
Critical pair: abbbbcb=cdbcbbbba.
Reduce RHS:
| [26] | (cd)bcbbbba |
| ⇒ bcbbbba |
Flip LHS and RHS.
Defines rule #17.
Referenced by [54].
Overlap of [39] adbcbbbba=bbbbcb with [15] babcbbbb=d:
Critical pair: adbcbbbd=bbbbcbbcbbbb.
Flip LHS and RHS.
Defines rule #37.
Referenced by [55].
Overlap of [39] adbcbbbba=bbbbcb with [17] babcbd=dbcbab:
Critical pair: adbcbbbdbcbab=bbbbcbbcbd.
Flip LHS and RHS.
Defines rule #25.
Overlap of [39] adbcbbbba=bbbbcb with [18] babcbbd=dbbcbab:
Critical pair: adbcbbbdbbcbab=bbbbcbbcbbd.
Flip LHS and RHS.
Defines rule #30.
Referenced by [58].
Overlap of [39] adbcbbbba=bbbbcb with [28] babcbad=dbcbaba:
Critical pair: adbcbbbdbcbaba=bbbbcbbcbad.
Flip LHS and RHS.
Defines rule #27.
Overlap of [40] abcbbba=bbbcbc with [33] babcbbad=dbbcbaba:
Critical pair: abcbbdbbcbaba=bbbcbcbcbbad.
Flip LHS and RHS.
Defines rule #26.
Overlap of [29] bcbabc=cbabcb with [30] babcbbabc=dbcbacbabcb:
Critical pair: bcdbcbacbabcb=cbabcbbbabc.
Reduce LHS:
| [26] | b(cd)bcbacbabcb |
| ⇒ bbcbacbabcb |
Reduce RHS:
| [45] | cba(bcbbba)bc |
| [2] | ⇒ cb(aa)dbbbcbcbc |
| [26] | ⇒ cb(cd)bbbcbcbc |
| ⇒ cbbbbcbcbc |
Flip LHS and RHS.
Referenced by [56].
Overlap of [45] bcbbba=adbbbcbc with [30] babcbbabc=dbcbacbabcb:
Critical pair: bcbbdbcbacbabcb=adbbbcbcbcbbabc.
Flip LHS and RHS.
Referenced by [59].
Overlap of [46] bcbbbba=abbbbcb with [30] babcbbabc=dbcbacbabcb:
Critical pair: bcbbbdbcbacbabcb=abbbbcbbcbbabc.
Flip LHS and RHS.
Referenced by [61].
Overlap of [15] babcbbbb=d with [47] bbbbcbbcbbbb=adbcbbbd:
Critical pair: babcbbbadbcbbbd=dbbbcbbcbbbb.
Reduce LHS:
| [45] | ba(bcbbba)dbcbbbd |
| [2] | ⇒ b(aa)dbbbcbcdbcbbbd |
| [26] | ⇒ b(cd)bbbcbcdbcbbbd |
| [26] | ⇒ bbbbcb(cd)bcbbbd |
| ⇒ bbbbcbbcbbbd |
Defines rule #35.
Overlap of [16] dc=1 with [52] cbbbbcbcbc=bbcbacbabcb:
Critical pair: dbbcbacbabcb=bbbbcbcbc.
Flip LHS and RHS.
Defines rule #20.
Referenced by [57].
Overlap of [56] bbbbcbcbc=dbbcbacbabcb with [5] ca=ac:
Critical pair: bbbbcbcbac=dbbcbacbabcba.
Defines rule #22.
Overlap of [49] bbbbcbbcbbd=adbcbbbdbbcbab with [23] da=ad:
Critical pair: bbbbcbbcbbad=adbcbbbdbbcbaba.
Defines rule #32.
Overlap of [2] aa=c with [53] adbbbcbcbcbbabc=bcbbdbcbacbabcb:
Critical pair: abcbbdbcbacbabcb=cdbbbcbcbcbbabc.
Reduce RHS:
| [26] | (cd)bbbcbcbcbbabc |
| ⇒ bbbcbcbcbbabc |
Flip LHS and RHS.
Defines rule #28.
Referenced by [60].
Overlap of [59] bbbcbcbcbbabc=abcbbdbcbacbabcb with [5] ca=ac:
Critical pair: bbbcbcbcbbabac=abcbbdbcbacbabcba.
Defines rule #31.
Overlap of [2] aa=c with [54] abbbbcbbcbbabc=bcbbbdbcbacbabcb:
Critical pair: abcbbbdbcbacbabcb=cbbbbcbbcbbabc.
Flip LHS and RHS.
Referenced by [62].
Overlap of [16] dc=1 with [61] cbbbbcbbcbbabc=abcbbbdbcbacbabcb:
Critical pair: dabcbbbdbcbacbabcb=bbbbcbbcbbabc.
Reduce LHS:
| [23] | (da)bcbbbdbcbacbabcb |
| ⇒ adbcbbbdbcbacbabcb |
Flip LHS and RHS.
Defines rule #34.
Referenced by [63].
Overlap of [62] bbbbcbbcbbabc=adbcbbbdbcbacbabcb with [5] ca=ac:
Critical pair: bbbbcbbcbbabac=adbcbbbdbcbacbabcba.
Defines rule #36.