| Back: | ⟨a, b | aaabbbabba=1⟩ |
|---|
Completion settings:
Axiom: aaabbbabba=1.
Referenced by [4].
Axiom: aaaa=c.
Defines rule #5.
Referenced by [5], [6], [7], [9], [11], [19], [25], [27], [33], [34], [39].
Axiom: bbbabb=d.
Defines rule #19.
Referenced by [4], [21], [22], [27], [32].
Overlap of [1] aaabbbabba=1 with [3] bbbabb=d:
Critical pair: aaada=1.
Referenced by [6], [7], [8], [10], [11], [12], [14], [16].
Overlap of [2] aaaa=c with [2] aaaa=c:
Critical pair: ac=ca.
Defines rule #3.
Referenced by [12], [15], [26], [35].
Overlap of [2] aaaa=c with [4] aaada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Referenced by [9], [10], [11], [13], [14].
Overlap of [2] aaaa=c with [4] aaada=1:
Critical pair: aa=cada.
Flip LHS and RHS.
Referenced by [11].
Overlap of [4] aaada=1 with [4] aaada=1:
Critical pair: aaad=aada.
Referenced by [10], [12], [16].
Overlap of [6] cda=a with [2] aaaa=c:
Critical pair: cdc=aaaa.
Reduce RHS:
| [2] | (aaaa) |
| ⇒ c |
Referenced by [13].
Overlap of [6] cda=a with [4] aaada=1:
Critical pair: cd=aaada.
Reduce RHS:
| [8] | (aaad)a |
| ⇒ aadaa |
Flip LHS and RHS.
Referenced by [12], [13], [14], [15].
Overlap of [7] cada=aa with [4] aaada=1:
Critical pair: cad=aaaada.
Reduce RHS:
| [2] | (aaaa)da |
| [6] | ⇒ (cda) |
| ⇒ a |
Referenced by [12], [15], [20].
Overlap of [4] aaada=1 with [10] aadaa=cd:
Critical pair: aaadcd=adaa.
Reduce LHS:
| [8] | (aaad)cd |
| [5] | ⇒ aad(ac)d |
| [11] | ⇒ aad(cad) |
| ⇒ aada |
Referenced by [13].
Overlap of [6] cda=a with [10] aadaa=cd:
Critical pair: cdcd=aadaa.
Reduce LHS:
| [9] | (cdc)d |
| ⇒ cd |
Reduce RHS:
| [12] | (aada)a |
| ⇒ adaaa |
Flip LHS and RHS.
Overlap of [10] aadaa=cd with [4] aaada=1:
Critical pair: aad=cdada.
Reduce RHS:
| [6] | (cda)da |
| ⇒ ada |
Overlap of [10] aadaa=cd with [10] aadaa=cd:
Critical pair: aadcd=cddaa.
Reduce LHS:
| [14] | (aad)cd |
| [5] | ⇒ ad(ac)d |
| [11] | ⇒ ad(cad) |
| ⇒ ada |
Flip LHS and RHS.
Referenced by [18].
Overlap of [4] aaada=1 with [8] aaad=aada:
Critical pair: aadaa=1.
Reduce LHS:
| [14] | (aad)aa |
| [13] | ⇒ (adaaa) |
| ⇒ cd |
Defines rule #1.
Referenced by [17], [18], [23], [27], [33], [36], [41].
Simplify [13] adaaa=cd.
Reduce RHS:
| [16] | (cd) |
| ⇒ 1 |
Referenced by [19].
Overlap of [15] cddaa=ada with [16] cd=1:
Critical pair: daa=ada.
Flip LHS and RHS.
Referenced by [19].
Simplify [17] adaaa=1.
Reduce LHS:
| [18] | (ada)aa |
| [2] | ⇒ d(aaaa) |
| ⇒ dc |
Defines rule #2.
Referenced by [20], [25], [38], [39].
Overlap of [19] dc=1 with [11] cad=a:
Critical pair: da=ad.
Flip LHS and RHS.
Defines rule #4.
Referenced by [21], [24], [29], [30], [38], [40].
Overlap of [3] bbbabb=d with [3] bbbabb=d:
Critical pair: bbbad=dbabb.
Reduce LHS:
| [20] | bbb(ad) |
| ⇒ bbbda |
Flip LHS and RHS.
Defines rule #7.
Overlap of [3] bbbabb=d with [3] bbbabb=d:
Critical pair: bbbabd=dbbabb.
Flip LHS and RHS.
Defines rule #15.
Referenced by [30].
Overlap of [16] cd=1 with [21] dbabb=bbbda:
Critical pair: cbbbda=babb.
Referenced by [25].
Overlap of [20] ad=da with [21] dbabb=bbbda:
Critical pair: abbbda=dababb.
Flip LHS and RHS.
Defines rule #10.
Referenced by [29].
Overlap of [23] cbbbda=babb with [2] aaaa=c:
Critical pair: cbbbdc=babbaaa.
Reduce LHS:
| [19] | cbbb(dc) |
| ⇒ cbbb |
Defines rule #6.
Referenced by [26], [27], [33].
Overlap of [5] ac=ca with [25] cbbb=babbaaa:
Critical pair: ababbaaa=cabbb.
Flip LHS and RHS.
Defines rule #9.
Referenced by [35].
Overlap of [25] cbbb=babbaaa with [3] bbbabb=d:
Critical pair: cd=babbaaaabb.
Reduce LHS:
| [16] | (cd) |
| ⇒ 1 |
Reduce RHS:
| [2] | babb(aaaa)bb |
| ⇒ babbcbb |
Flip LHS and RHS.
Overlap of [27] babbcbb=1 with [27] babbcbb=1:
Critical pair: babbcb=abbcbb.
Flip LHS and RHS.
Referenced by [31].
Overlap of [20] ad=da with [24] dababb=abbbda:
Critical pair: aabbbda=daababb.
Flip LHS and RHS.
Defines rule #12.
Referenced by [38].
Overlap of [20] ad=da with [22] dbbabb=bbbabd:
Critical pair: abbbabd=dabbabb.
Flip LHS and RHS.
Defines rule #16.
Referenced by [40].
Overlap of [27] babbcbb=1 with [28] abbcbb=babbcb:
Critical pair: bbabbcb=1.
Referenced by [32].
Overlap of [3] bbbabb=d with [31] bbabbcb=1:
Critical pair: bbba=dabbcb.
Flip LHS and RHS.
Referenced by [33].
Overlap of [16] cd=1 with [32] dabbcb=bbba:
Critical pair: cbbba=abbcb.
Reduce LHS:
| [25] | (cbbb)a |
| [2] | ⇒ babb(aaaa) |
| ⇒ babbc |
Flip LHS and RHS.
Defines rule #8.
Overlap of [2] aaaa=c with [33] abbcb=babbc:
Critical pair: aaababbc=cbbcb.
Overlap of [5] ac=ca with [26] cabbb=ababbaaa:
Critical pair: aababbaaa=caabbb.
Flip LHS and RHS.
Defines rule #11.
Overlap of [34] aaababbc=cbbcb with [16] cd=1:
Critical pair: aaababb=cbbcbd.
Defines rule #14.
Referenced by [38].
Overlap of [34] aaababbc=cbbcb with [33] abbcb=babbc:
Critical pair: aaabbabbc=cbbcbb.
Referenced by [41].
Overlap of [20] ad=da with [29] daababb=aabbbda:
Critical pair: aaabbbda=daaababb.
Reduce RHS:
| [36] | d(aaababb) |
| [19] | ⇒ (dc)bbcbd |
| ⇒ bbcbd |
Referenced by [39].
Overlap of [38] aaabbbda=bbcbd with [2] aaaa=c:
Critical pair: aaabbbdc=bbcbdaaa.
Reduce LHS:
| [19] | aaabbb(dc) |
| ⇒ aaabbb |
Defines rule #13.
Overlap of [20] ad=da with [30] dabbabb=abbbabd:
Critical pair: aabbbabd=daabbabb.
Flip LHS and RHS.
Defines rule #17.
Overlap of [37] aaabbabbc=cbbcbb with [16] cd=1:
Critical pair: aaabbabb=cbbcbbd.
Defines rule #18.