| Back: | ⟨a, b | aaabaaabbba=1⟩ |
|---|
Completion settings:
Axiom: aaabaaabbba=1.
Referenced by [4].
Axiom: aaaa=c.
Defines rule #5.
Referenced by [5], [6], [11], [15], [17], [20], [26], [28], [37].
Axiom: baaabbb=d.
Defines rule #13.
Referenced by [4], [12], [17], [19], [25], [30].
Overlap of [1] aaabaaabbba=1 with [3] baaabbb=d:
Critical pair: aaada=1.
Referenced by [6], [7], [8], [9], [10], [11].
Overlap of [2] aaaa=c with [2] aaaa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #3.
Referenced by [16], [22], [25], [26], [27], [35].
Overlap of [2] aaaa=c with [4] aaada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Referenced by [8].
Overlap of [4] aaada=1 with [4] aaada=1:
Critical pair: aaad=aada.
Flip LHS and RHS.
Referenced by [9], [10], [11], [12].
Overlap of [6] cda=a with [4] aaada=1:
Critical pair: cd=aaada.
Reduce RHS:
| [4] | (aaada) |
| ⇒ 1 |
Defines rule #2.
Referenced by [15], [20], [22], [26], [37], [38].
Overlap of [4] aaada=1 with [7] aada=aaad:
Critical pair: aaadaaad=ada.
Reduce LHS:
| [4] | (aaada)aad |
| ⇒ aad |
Flip LHS and RHS.
Referenced by [11].
Overlap of [7] aada=aaad with [7] aada=aaad:
Critical pair: aadaaad=aaadada.
Reduce LHS:
| [7] | (aada)aad |
| [4] | ⇒ (aaada)ad |
| ⇒ ad |
Reduce RHS:
| [4] | (aaada)da |
| ⇒ da |
Flip LHS and RHS.
Defines rule #4.
Referenced by [11], [12], [13], [20], [29], [34].
Overlap of [10] da=ad with [2] aaaa=c:
Critical pair: dc=adaaa.
Reduce RHS:
| [9] | (ada)aa |
| [7] | ⇒ (aada)a |
| [4] | ⇒ (aaada) |
| ⇒ 1 |
Defines rule #1.
Referenced by [14], [17], [21], [23], [24], [34].
Overlap of [3] baaabbb=d with [3] baaabbb=d:
Critical pair: baaabbd=daaabbb.
Reduce RHS:
| [10] | (da)aabbb |
| [10] | ⇒ a(da)abbb |
| [7] | ⇒ (aada)bbb |
| ⇒ aaadbbb |
Defines rule #9.
Referenced by [13], [14], [26], [31].
Overlap of [12] baaabbd=aaadbbb with [10] da=ad:
Critical pair: baaabbad=aaadbbba.
Referenced by [22].
Overlap of [12] baaabbd=aaadbbb with [11] dc=1:
Critical pair: baaabb=aaadbbbc.
Flip LHS and RHS.
Overlap of [2] aaaa=c with [14] aaadbbbc=baaabb:
Critical pair: abaaabb=cdbbbc.
Reduce RHS:
| [8] | (cd)bbbc |
| ⇒ bbbc |
Flip LHS and RHS.
Defines rule #8.
Referenced by [17].
Overlap of [14] aaadbbbc=baaabb with [5] ca=ac:
Critical pair: aaadbbbac=baaabba.
Referenced by [33].
Overlap of [3] baaabbb=d with [15] bbbc=abaaabb:
Critical pair: baaaabaaabb=dc.
Reduce LHS:
| [2] | b(aaaa)baaabb |
| ⇒ bcbaaabb |
Reduce RHS:
| [11] | (dc) |
| ⇒ 1 |
Referenced by [18].
Overlap of [17] bcbaaabb=1 with [17] bcbaaabb=1:
Critical pair: bcbaaab=cbaaabb.
Overlap of [18] bcbaaab=cbaaabb with [3] baaabbb=d:
Critical pair: bcbaaad=cbaaabbaaabbb.
Reduce RHS:
| [3] | cbaaab(baaabbb) |
| ⇒ cbaaabd |
Overlap of [19] bcbaaad=cbaaabd with [10] da=ad:
Critical pair: bcbaaaad=cbaaabda.
Reduce LHS:
| [2] | bcb(aaaa)d |
| [8] | ⇒ bcb(cd) |
| ⇒ bcb |
Reduce RHS:
| [10] | cbaaab(da) |
| ⇒ cbaaabad |
Flip LHS and RHS.
Overlap of [19] bcbaaad=cbaaabd with [11] dc=1:
Critical pair: bcbaaa=cbaaabdc.
Reduce RHS:
| [11] | cbaaab(dc) |
| ⇒ cbaaab |
Defines rule #7.
Overlap of [18] bcbaaab=cbaaabb with [20] cbaaabad=bcb:
Critical pair: bbcb=cbaaabbad.
Reduce RHS:
| [13] | c(baaabbad) |
| [5] | ⇒ (ca)aadbbba |
| [5] | ⇒ a(ca)adbbba |
| [5] | ⇒ aa(ca)dbbba |
| [8] | ⇒ aaa(cd)bbba |
| ⇒ aaabbba |
Flip LHS and RHS.
Referenced by [28], [29], [30], [31], [32].
Overlap of [20] cbaaabad=bcb with [11] dc=1:
Critical pair: cbaaaba=bcbc.
Referenced by [24], [25], [26], [27].
Overlap of [11] dc=1 with [23] cbaaaba=bcbc:
Critical pair: dbcbc=baaaba.
Flip LHS and RHS.
Defines rule #6.
Referenced by [27], [32], [35].
Overlap of [23] cbaaaba=bcbc with [3] baaabbb=d:
Critical pair: cbaaad=bcbcaabbb.
Reduce RHS:
| [5] | bcb(ca)abbb |
| [5] | ⇒ bcba(ca)bbb |
| ⇒ bcbaacbbb |
Flip LHS and RHS.
Defines rule #17.
Overlap of [23] cbaaaba=bcbc with [12] baaabbd=aaadbbb:
Critical pair: cbaaaaaadbbb=bcbcaabbd.
Reduce LHS:
| [2] | cb(aaaa)aadbbb |
| [5] | ⇒ cb(ca)adbbb |
| [5] | ⇒ cba(ca)dbbb |
| [8] | ⇒ cbaa(cd)bbb |
| ⇒ cbaabbb |
Reduce RHS:
| [5] | bcb(ca)abbd |
| [5] | ⇒ bcba(ca)bbd |
| ⇒ bcbaacbbd |
Flip LHS and RHS.
Defines rule #14.
Overlap of [23] cbaaaba=bcbc with [24] baaaba=dbcbc:
Critical pair: cbaaadbcbc=bcbcaaba.
Reduce RHS:
| [5] | bcb(ca)aba |
| [5] | ⇒ bcba(ca)ba |
| ⇒ bcbaacba |
Flip LHS and RHS.
Defines rule #12.
Overlap of [2] aaaa=c with [22] aaabbba=bbcb:
Critical pair: abbcb=cbbba.
Flip LHS and RHS.
Referenced by [34].
Overlap of [10] da=ad with [22] aaabbba=bbcb:
Critical pair: dbbcb=adaabbba.
Reduce RHS:
| [10] | a(da)abbba |
| [10] | ⇒ aa(da)bbba |
| ⇒ aaadbbba |
Flip LHS and RHS.
Referenced by [33].
Overlap of [22] aaabbba=bbcb with [3] baaabbb=d:
Critical pair: aaabbd=bbcbaabbb.
Flip LHS and RHS.
Defines rule #20.
Overlap of [22] aaabbba=bbcb with [12] baaabbd=aaadbbb:
Critical pair: aaabbaaadbbb=bbcbaabbd.
Flip LHS and RHS.
Defines rule #18.
Overlap of [22] aaabbba=bbcb with [24] baaaba=dbcbc:
Critical pair: aaabbdbcbc=bbcbaaba.
Flip LHS and RHS.
Defines rule #16.
Overlap of [16] aaadbbbac=baaabba with [29] aaadbbba=dbbcb:
Critical pair: dbbcbc=baaabba.
Flip LHS and RHS.
Defines rule #11.
Overlap of [11] dc=1 with [28] cbbba=abbcb:
Critical pair: dabbcb=bbba.
Reduce LHS:
| [10] | (da)bbcb |
| ⇒ adbbcb |
Flip LHS and RHS.
Defines rule #10.
Referenced by [36].
Overlap of [24] baaaba=dbcbc with [33] baaabba=dbbcbc:
Critical pair: baaadbbcbc=dbcbcaabba.
Reduce RHS:
| [5] | dbcb(ca)abba |
| [5] | ⇒ dbcba(ca)bba |
| ⇒ dbcbaacbba |
Flip LHS and RHS.
Referenced by [38].
Overlap of [34] bbba=adbbcb with [33] baaabba=dbbcbc:
Critical pair: bbdbbcbc=adbbcbaabba.
Flip LHS and RHS.
Referenced by [37].
Overlap of [2] aaaa=c with [36] adbbcbaabba=bbdbbcbc:
Critical pair: aaabbdbbcbc=cdbbcbaabba.
Reduce RHS:
| [8] | (cd)bbcbaabba |
| ⇒ bbcbaabba |
Flip LHS and RHS.
Defines rule #19.
Overlap of [8] cd=1 with [35] dbcbaacbba=baaadbbcbc:
Critical pair: cbaaadbbcbc=bcbaacbba.
Flip LHS and RHS.
Defines rule #15.