| Back: | ⟨a, b | aaaabbbabba=1⟩ |
|---|
Completion settings:
Axiom: aaaabbbabba=1.
Referenced by [4].
Axiom: aaaaa=c.
Defines rule #5.
Referenced by [5], [6], [7], [10], [16], [18], [20], [25], [27], [28], [31], [39].
Axiom: bbbabb=d.
Defines rule #22.
Referenced by [4], [11], [12], [27].
Overlap of [1] aaaabbbabba=1 with [3] bbbabb=d:
Critical pair: aaaada=1.
Referenced by [6], [7], [8], [9], [10], [13].
Overlap of [2] aaaaa=c with [2] aaaaa=c:
Critical pair: ac=ca.
Defines rule #3.
Referenced by [26], [33], [37].
Overlap of [2] aaaaa=c with [4] aaaada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Overlap of [2] aaaaa=c with [4] aaaada=1:
Critical pair: aa=cada.
Flip LHS and RHS.
Referenced by [10].
Overlap of [4] aaaada=1 with [4] aaaada=1:
Critical pair: aaaad=aaada.
Referenced by [9], [13], [20].
Overlap of [6] cda=a with [4] aaaada=1:
Critical pair: cd=aaaada.
Reduce RHS:
| [8] | (aaaad)a |
| ⇒ aaadaa |
Flip LHS and RHS.
Overlap of [7] cada=aa with [4] aaaada=1:
Critical pair: cad=aaaaada.
Reduce RHS:
| [2] | (aaaaa)da |
| [6] | ⇒ (cda) |
| ⇒ a |
Referenced by [19].
Overlap of [3] bbbabb=d with [3] bbbabb=d:
Critical pair: bbbad=dbabb.
Flip LHS and RHS.
Referenced by [21].
Overlap of [3] bbbabb=d with [3] bbbabb=d:
Critical pair: bbbabd=dbbabb.
Flip LHS and RHS.
Defines rule #17.
Overlap of [4] aaaada=1 with [8] aaaad=aaada:
Critical pair: aaadaa=1.
Reduce LHS:
| [9] | (aaadaa) |
| ⇒ cd |
Defines rule #1.
Referenced by [14], [16], [20], [22], [27], [28], [41].
Simplify [9] aaadaa=cd.
Reduce RHS:
| [13] | (cd) |
| ⇒ 1 |
Overlap of [14] aaadaa=1 with [14] aaadaa=1:
Critical pair: aaad=adaa.
Referenced by [16], [17], [20].
Overlap of [2] aaaaa=c with [15] aaad=adaa:
Critical pair: aaadaa=cd.
Reduce LHS:
| [15] | (aaad)aa |
| ⇒ adaaaa |
Reduce RHS:
| [13] | (cd) |
| ⇒ 1 |
Overlap of [14] aaadaa=1 with [15] aaad=adaa:
Critical pair: aaadaadaa=aad.
Reduce LHS:
| [15] | (aaad)aadaa |
| [16] | ⇒ (adaaaa)daa |
| ⇒ daa |
Flip LHS and RHS.
Overlap of [17] aad=daa with [16] adaaaa=1:
Critical pair: a=daaaaaa.
Reduce RHS:
| [2] | d(aaaaa)a |
| ⇒ dca |
Flip LHS and RHS.
Referenced by [19].
Overlap of [18] dca=a with [10] cad=a:
Critical pair: da=ad.
Flip LHS and RHS.
Defines rule #4.
Referenced by [20], [21], [24], [29], [34], [36], [38], [40].
Overlap of [2] aaaaa=c with [19] ad=da:
Critical pair: aaaada=cd.
Reduce LHS:
| [8] | (aaaad)a |
| [15] | ⇒ (aaad)aa |
| [19] | ⇒ (ad)aaaa |
| [2] | ⇒ d(aaaaa) |
| ⇒ dc |
Reduce RHS:
| [13] | (cd) |
| ⇒ 1 |
Defines rule #2.
Referenced by [25], [32], [35], [38], [39].
Simplify [11] dbabb=bbbad.
Reduce RHS:
| [19] | bbb(ad) |
| ⇒ bbbda |
Defines rule #7.
Referenced by [22], [23], [24].
Overlap of [13] cd=1 with [21] dbabb=bbbda:
Critical pair: cbbbda=babb.
Referenced by [25].
Overlap of [17] aad=daa with [21] dbabb=bbbda:
Critical pair: aabbbda=daababb.
Flip LHS and RHS.
Defines rule #12.
Referenced by [34].
Overlap of [19] ad=da with [21] dbabb=bbbda:
Critical pair: abbbda=dababb.
Flip LHS and RHS.
Defines rule #10.
Overlap of [22] cbbbda=babb with [2] aaaaa=c:
Critical pair: cbbbdc=babbaaaa.
Reduce LHS:
| [20] | cbbb(dc) |
| ⇒ cbbb |
Defines rule #6.
Referenced by [26], [27], [28].
Overlap of [5] ac=ca with [25] cbbb=babbaaaa:
Critical pair: ababbaaaa=cabbb.
Flip LHS and RHS.
Defines rule #9.
Referenced by [33].
Overlap of [25] cbbb=babbaaaa with [3] bbbabb=d:
Critical pair: cd=babbaaaaabb.
Reduce LHS:
| [13] | (cd) |
| ⇒ 1 |
Reduce RHS:
| [2] | babb(aaaaa)bb |
| ⇒ babbcbb |
Flip LHS and RHS.
Referenced by [30].
Overlap of [13] cd=1 with [12] dbbabb=bbbabd:
Critical pair: cbbbabd=bbabb.
Reduce LHS:
| [25] | (cbbb)abd |
| [2] | ⇒ babb(aaaaa)bd |
| ⇒ babbcbd |
Referenced by [30].
Overlap of [19] ad=da with [12] dbbabb=bbbabd:
Critical pair: abbbabd=dabbabb.
Flip LHS and RHS.
Defines rule #18.
Referenced by [36].
Overlap of [27] babbcbb=1 with [28] babbcbd=bbabb:
Critical pair: babbcbbbabb=abbcbd.
Reduce LHS:
| [27] | (babbcbb)babb |
| ⇒ babb |
Flip LHS and RHS.
Overlap of [2] aaaaa=c with [30] abbcbd=babb:
Critical pair: aaaababb=cbbcbd.
Defines rule #16.
Overlap of [30] abbcbd=babb with [20] dc=1:
Critical pair: abbcb=babbc.
Defines rule #8.
Referenced by [35].
Overlap of [5] ac=ca with [26] cabbb=ababbaaaa:
Critical pair: aababbaaaa=caabbb.
Flip LHS and RHS.
Defines rule #11.
Referenced by [37].
Overlap of [19] ad=da with [23] daababb=aabbbda:
Critical pair: aaabbbda=daaababb.
Flip LHS and RHS.
Defines rule #14.
Referenced by [38].
Overlap of [31] aaaababb=cbbcbd with [32] abbcb=babbc:
Critical pair: aaaabbabbc=cbbcbdcb.
Reduce RHS:
| [20] | cbbcb(dc)b |
| ⇒ cbbcbb |
Referenced by [41].
Overlap of [19] ad=da with [29] dabbabb=abbbabd:
Critical pair: aabbbabd=daabbabb.
Flip LHS and RHS.
Defines rule #19.
Referenced by [40].
Overlap of [5] ac=ca with [33] caabbb=aababbaaaa:
Critical pair: aaababbaaaa=caaabbb.
Flip LHS and RHS.
Defines rule #13.
Overlap of [19] ad=da with [34] daaababb=aaabbbda:
Critical pair: aaaabbbda=daaaababb.
Reduce RHS:
| [31] | d(aaaababb) |
| [20] | ⇒ (dc)bbcbd |
| ⇒ bbcbd |
Referenced by [39].
Overlap of [38] aaaabbbda=bbcbd with [2] aaaaa=c:
Critical pair: aaaabbbdc=bbcbdaaaa.
Reduce LHS:
| [20] | aaaabbb(dc) |
| ⇒ aaaabbb |
Defines rule #15.
Overlap of [19] ad=da with [36] daabbabb=aabbbabd:
Critical pair: aaabbbabd=daaabbabb.
Flip LHS and RHS.
Defines rule #20.
Overlap of [35] aaaabbabbc=cbbcbb with [13] cd=1:
Critical pair: aaaabbabb=cbbcbbd.
Defines rule #21.