| Back: | ⟨a, b | aaabbbaaaba=1⟩ |
|---|
Completion settings:
Axiom: aaabbbaaaba=1.
Referenced by [4].
Axiom: aaaa=c.
Defines rule #5.
Referenced by [5], [6], [7], [9], [11], [19], [24], [26], [30], [33], [35], [47], [48], [50], [52].
Axiom: bbbaaab=d.
Defines rule #13.
Referenced by [4], [21], [26], [34].
Overlap of [1] aaabbbaaaba=1 with [3] bbbaaab=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], [25], [29], [34], [35], [38], [40], [41].
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], [22], [26], [36], [39].
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], [24], [30], [35], [42], [46], [47], [48], [49], [50], [51], [52].
Overlap of [19] dc=1 with [11] cad=a:
Critical pair: da=ad.
Flip LHS and RHS.
Defines rule #4.
Overlap of [3] bbbaaab=d with [3] bbbaaab=d:
Critical pair: bbbaaad=dbbaaab.
Reduce LHS:
| [20] | bbbaa(ad) |
| [20] | ⇒ bbba(ad)a |
| [20] | ⇒ bbb(ad)aa |
| ⇒ bbbdaaa |
Flip LHS and RHS.
Defines rule #9.
Referenced by [22], [23], [27], [30], [35], [43].
Overlap of [16] cd=1 with [21] dbbaaab=bbbdaaa:
Critical pair: cbbbdaaa=bbaaab.
Referenced by [24].
Overlap of [20] ad=da with [21] dbbaaab=bbbdaaa:
Critical pair: abbbdaaa=dabbaaab.
Flip LHS and RHS.
Referenced by [46].
Overlap of [22] cbbbdaaa=bbaaab with [2] aaaa=c:
Critical pair: cbbbdc=bbaaaba.
Reduce LHS:
| [19] | cbbb(dc) |
| ⇒ cbbb |
Defines rule #8.
Overlap of [5] ac=ca with [24] cbbb=bbaaaba:
Critical pair: abbaaaba=cabbb.
Flip LHS and RHS.
Referenced by [29].
Overlap of [24] cbbb=bbaaaba with [3] bbbaaab=d:
Critical pair: cd=bbaaabaaaab.
Reduce LHS:
| [16] | (cd) |
| ⇒ 1 |
Reduce RHS:
| [2] | bbaaab(aaaa)b |
| ⇒ bbaaabcb |
Flip LHS and RHS.
Referenced by [27], [28], [31].
Overlap of [21] dbbaaab=bbbdaaa with [26] bbaaabcb=1:
Critical pair: dbbaaa=bbbdaaabaaabcb.
Flip LHS and RHS.
Referenced by [32].
Overlap of [26] bbaaabcb=1 with [26] bbaaabcb=1:
Critical pair: bbaaabc=baaabcb.
Flip LHS and RHS.
Overlap of [5] ac=ca with [25] cabbb=abbaaaba:
Critical pair: aabbaaaba=caabbb.
Flip LHS and RHS.
Referenced by [41].
Overlap of [21] dbbaaab=bbbdaaa with [28] baaabcb=bbaaabc:
Critical pair: dbbaaabbaaabc=bbbdaaaaaabcb.
Reduce LHS:
| [21] | (dbbaaab)baaabc |
| ⇒ bbbdaaabaaabc |
Reduce RHS:
| [2] | bbbd(aaaa)aabcb |
| [19] | ⇒ bbb(dc)aabcb |
| ⇒ bbbaabcb |
Referenced by [32].
Overlap of [26] bbaaabcb=1 with [28] baaabcb=bbaaabc:
Critical pair: bbaaabcbbaaabc=aaabcb.
Reduce LHS:
| [26] | (bbaaabcb)baaabc |
| ⇒ baaabc |
Flip LHS and RHS.
Defines rule #7.
Overlap of [27] bbbdaaabaaabcb=dbbaaa with [30] bbbdaaabaaabc=bbbaabcb:
Critical pair: bbbaabcbb=dbbaaa.
Defines rule #20.
Overlap of [2] aaaa=c with [31] aaabcb=baaabc:
Critical pair: abaaabc=cbcb.
Referenced by [34], [35], [36], [37].
Overlap of [3] bbbaaab=d with [33] abaaabc=cbcb:
Critical pair: bbbaacbcb=daaabc.
Reduce LHS:
| [5] | bbba(ac)bcb |
| [5] | ⇒ bbb(ac)abcb |
| ⇒ bbbcaabcb |
Defines rule #17.
Overlap of [21] dbbaaab=bbbdaaa with [33] abaaabc=cbcb:
Critical pair: dbbaacbcb=bbbdaaaaaabc.
Reduce LHS:
| [5] | dbba(ac)bcb |
| [5] | ⇒ dbb(ac)abcb |
| ⇒ dbbcaabcb |
Reduce RHS:
| [2] | bbbd(aaaa)aabc |
| [19] | ⇒ bbb(dc)aabc |
| ⇒ bbbaabc |
Defines rule #14.
Overlap of [33] abaaabc=cbcb with [16] cd=1:
Critical pair: abaaab=cbcbd.
Defines rule #6.
Referenced by [38], [40], [44].
Overlap of [33] abaaabc=cbcb with [31] aaabcb=baaabc:
Critical pair: abbaaabc=cbcbb.
Referenced by [39].
Overlap of [36] abaaab=cbcbd with [36] abaaab=cbcbd:
Critical pair: abaacbcbd=cbcbdaaab.
Reduce LHS:
| [5] | aba(ac)bcbd |
| [5] | ⇒ ab(ac)abcbd |
| ⇒ abcaabcbd |
Referenced by [49].
Overlap of [37] abbaaabc=cbcbb with [16] cd=1:
Critical pair: abbaaab=cbcbbd.
Defines rule #11.
Referenced by [40], [41], [45], [46].
Overlap of [39] abbaaab=cbcbbd with [36] abaaab=cbcbd:
Critical pair: abbaacbcbd=cbcbbdaaab.
Reduce LHS:
| [5] | abba(ac)bcbd |
| [5] | ⇒ abb(ac)abcbd |
| ⇒ abbcaabcbd |
Referenced by [51].
Simplify [29] caabbb=aabbaaaba.
Reduce RHS:
| [39] | a(abbaaab)a |
| [5] | ⇒ (ac)bcbbda |
| ⇒ cabcbbda |
Referenced by [42].
Overlap of [19] dc=1 with [41] caabbb=cabcbbda:
Critical pair: dcabcbbda=aabbb.
Reduce LHS:
| [19] | (dc)abcbbda |
| ⇒ abcbbda |
Flip LHS and RHS.
Referenced by [43], [44], [45].
Overlap of [21] dbbaaab=bbbdaaa with [42] aabbb=abcbbda:
Critical pair: dbbaabcbbda=bbbdaaabb.
Referenced by [52].
Overlap of [36] abaaab=cbcbd with [42] aabbb=abcbbda:
Critical pair: abaabcbbda=cbcbdbb.
Referenced by [48].
Overlap of [39] abbaaab=cbcbbd with [42] aabbb=abcbbda:
Critical pair: abbaabcbbda=cbcbbdbb.
Referenced by [50].
Simplify [23] dabbaaab=abbbdaaa.
Reduce LHS:
| [39] | d(abbaaab) |
| [19] | ⇒ (dc)bcbbd |
| ⇒ bcbbd |
Flip LHS and RHS.
Referenced by [47].
Overlap of [46] abbbdaaa=bcbbd with [2] aaaa=c:
Critical pair: abbbdc=bcbbda.
Reduce LHS:
| [19] | abbb(dc) |
| ⇒ abbb |
Defines rule #10.
Overlap of [44] abaabcbbda=cbcbdbb with [2] aaaa=c:
Critical pair: abaabcbbdc=cbcbdbbaaa.
Reduce LHS:
| [19] | abaabcbb(dc) |
| ⇒ abaabcbb |
Defines rule #16.
Overlap of [38] abcaabcbd=cbcbdaaab with [19] dc=1:
Critical pair: abcaabcb=cbcbdaaabc.
Defines rule #12.
Overlap of [45] abbaabcbbda=cbcbbdbb with [2] aaaa=c:
Critical pair: abbaabcbbdc=cbcbbdbbaaa.
Reduce LHS:
| [19] | abbaabcbb(dc) |
| ⇒ abbaabcbb |
Defines rule #19.
Overlap of [40] abbcaabcbd=cbcbbdaaab with [19] dc=1:
Critical pair: abbcaabcb=cbcbbdaaabc.
Defines rule #15.
Overlap of [43] dbbaabcbbda=bbbdaaabb with [2] aaaa=c:
Critical pair: dbbaabcbbdc=bbbdaaabbaaa.
Reduce LHS:
| [19] | dbbaabcbb(dc) |
| ⇒ dbbaabcbb |
Defines rule #18.