| Back: | ⟨a, b | aaaabbababa=1⟩ |
|---|
Completion settings:
Axiom: aaaabbababa=1.
Referenced by [4].
Axiom: aaaaa=c.
Defines rule #5.
Referenced by [5], [6], [7], [10], [15], [17], [19], [24], [26], [27], [28], [32], [36], [39].
Axiom: bbabab=d.
Defines rule #17.
Referenced by [4], [11], [26].
Overlap of [1] aaaabbababa=1 with [3] bbabab=d:
Critical pair: aaaada=1.
Referenced by [6], [7], [8], [9], [10], [12].
Overlap of [2] aaaaa=c with [2] aaaaa=c:
Critical pair: ac=ca.
Defines rule #3.
Referenced by [25], [28], [29], [33], [35], [40], [41], [42].
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], [12], [19].
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 [18].
Overlap of [3] bbabab=d with [3] bbabab=d:
Critical pair: bbabad=dbabab.
Flip LHS and RHS.
Referenced by [20].
Overlap of [4] aaaada=1 with [8] aaaad=aaada:
Critical pair: aaadaa=1.
Reduce LHS:
| [9] | (aaadaa) |
| ⇒ cd |
Defines rule #1.
Referenced by [13], [15], [19], [21], [26], [37].
Simplify [9] aaadaa=cd.
Reduce RHS:
| [12] | (cd) |
| ⇒ 1 |
Overlap of [13] aaadaa=1 with [13] aaadaa=1:
Critical pair: aaad=adaa.
Referenced by [15], [16], [19].
Overlap of [2] aaaaa=c with [14] aaad=adaa:
Critical pair: aaadaa=cd.
Reduce LHS:
| [14] | (aaad)aa |
| ⇒ adaaaa |
Reduce RHS:
| [12] | (cd) |
| ⇒ 1 |
Overlap of [13] aaadaa=1 with [14] aaad=adaa:
Critical pair: aaadaadaa=aad.
Reduce LHS:
| [14] | (aaad)aadaa |
| [15] | ⇒ (adaaaa)daa |
| ⇒ daa |
Flip LHS and RHS.
Overlap of [16] aad=daa with [15] adaaaa=1:
Critical pair: a=daaaaaa.
Reduce RHS:
| [2] | d(aaaaa)a |
| ⇒ dca |
Flip LHS and RHS.
Referenced by [18].
Overlap of [17] dca=a with [10] cad=a:
Critical pair: da=ad.
Flip LHS and RHS.
Defines rule #4.
Referenced by [19], [20], [23], [31], [34], [36], [38].
Overlap of [2] aaaaa=c with [18] ad=da:
Critical pair: aaaada=cd.
Reduce LHS:
| [8] | (aaaad)a |
| [14] | ⇒ (aaad)aa |
| [18] | ⇒ (ad)aaaa |
| [2] | ⇒ d(aaaaa) |
| ⇒ dc |
Reduce RHS:
| [12] | (cd) |
| ⇒ 1 |
Defines rule #2.
Referenced by [24], [30], [32], [36], [39].
Simplify [11] dbabab=bbabad.
Reduce RHS:
| [18] | bbab(ad) |
| ⇒ bbabda |
Defines rule #9.
Referenced by [21], [22], [23].
Overlap of [12] cd=1 with [20] dbabab=bbabda:
Critical pair: cbbabda=babab.
Referenced by [24].
Overlap of [16] aad=daa with [20] dbabab=bbabda:
Critical pair: aabbabda=daababab.
Flip LHS and RHS.
Defines rule #13.
Referenced by [34].
Overlap of [18] ad=da with [20] dbabab=bbabda:
Critical pair: abbabda=dababab.
Flip LHS and RHS.
Defines rule #11.
Overlap of [21] cbbabda=babab with [2] aaaaa=c:
Critical pair: cbbabdc=bababaaaa.
Reduce LHS:
| [19] | cbbab(dc) |
| ⇒ cbbab |
Defines rule #8.
Referenced by [25], [26], [27], [29].
Overlap of [5] ac=ca with [24] cbbab=bababaaaa:
Critical pair: abababaaaa=cabbab.
Flip LHS and RHS.
Defines rule #10.
Referenced by [33].
Overlap of [24] cbbab=bababaaaa with [3] bbabab=d:
Critical pair: cd=bababaaaaab.
Reduce LHS:
| [12] | (cd) |
| ⇒ 1 |
Reduce RHS:
| [2] | babab(aaaaa)b |
| ⇒ bababcb |
Flip LHS and RHS.
Referenced by [27].
Overlap of [24] cbbab=bababaaaa with [26] bababcb=1:
Critical pair: cbba=bababaaaaababcb.
Reduce RHS:
| [2] | babab(aaaaa)babcb |
| [26] | ⇒ (bababcb)abcb |
| ⇒ abcb |
Flip LHS and RHS.
Defines rule #6.
Overlap of [2] aaaaa=c with [27] abcb=cbba:
Critical pair: aaaacbba=cbcb.
Reduce LHS:
| [5] | aaa(ac)bba |
| [5] | ⇒ aa(ac)abba |
| [5] | ⇒ a(ac)aabba |
| [5] | ⇒ (ac)aaabba |
| ⇒ caaaabba |
Referenced by [30].
Overlap of [24] cbbab=bababaaaa with [27] abcb=cbba:
Critical pair: cbbcbba=bababaaaacb.
Reduce RHS:
| [5] | bababaaa(ac)b |
| [5] | ⇒ bababaa(ac)ab |
| [5] | ⇒ bababa(ac)aab |
| [5] | ⇒ babab(ac)aaab |
| ⇒ bababcaaaab |
Referenced by [38].
Overlap of [19] dc=1 with [28] caaaabba=cbcb:
Critical pair: dcbcb=aaaabba.
Reduce LHS:
| [19] | (dc)bcb |
| ⇒ bcb |
Flip LHS and RHS.
Referenced by [31].
Overlap of [30] aaaabba=bcb with [18] ad=da:
Critical pair: aaaabbda=bcbd.
Referenced by [32].
Overlap of [31] aaaabbda=bcbd with [2] aaaaa=c:
Critical pair: aaaabbdc=bcbdaaaa.
Reduce LHS:
| [19] | aaaabb(dc) |
| ⇒ aaaabb |
Defines rule #7.
Referenced by [36].
Overlap of [5] ac=ca with [25] cabbab=abababaaaa:
Critical pair: aabababaaaa=caabbab.
Flip LHS and RHS.
Defines rule #12.
Referenced by [35].
Overlap of [18] ad=da with [22] daababab=aabbabda:
Critical pair: aaabbabda=daaababab.
Flip LHS and RHS.
Defines rule #15.
Referenced by [36].
Overlap of [5] ac=ca with [33] caabbab=aabababaaaa:
Critical pair: aaabababaaaa=caaabbab.
Flip LHS and RHS.
Defines rule #14.
Overlap of [18] ad=da with [34] daaababab=aaabbabda:
Critical pair: aaaabbabda=daaaababab.
Reduce LHS:
| [32] | (aaaabb)abda |
| [2] | ⇒ bcbd(aaaaa)bda |
| [19] | ⇒ bcb(dc)bda |
| ⇒ bcbbda |
Flip LHS and RHS.
Referenced by [37].
Overlap of [12] cd=1 with [36] daaaababab=bcbbda:
Critical pair: cbcbbda=aaaababab.
Flip LHS and RHS.
Defines rule #16.
Overlap of [29] cbbcbba=bababcaaaab with [18] ad=da:
Critical pair: cbbcbbda=bababcaaaabd.
Referenced by [39].
Overlap of [38] cbbcbbda=bababcaaaabd with [2] aaaaa=c:
Critical pair: cbbcbbdc=bababcaaaabdaaaa.
Reduce LHS:
| [19] | cbbcbb(dc) |
| ⇒ cbbcbb |
Defines rule #18.
Referenced by [40].
Overlap of [5] ac=ca with [39] cbbcbb=bababcaaaabdaaaa:
Critical pair: abababcaaaabdaaaa=cabbcbb.
Flip LHS and RHS.
Defines rule #19.
Referenced by [41].
Overlap of [5] ac=ca with [40] cabbcbb=abababcaaaabdaaaa:
Critical pair: aabababcaaaabdaaaa=caabbcbb.
Flip LHS and RHS.
Defines rule #20.
Referenced by [42].
Overlap of [5] ac=ca with [41] caabbcbb=aabababcaaaabdaaaa:
Critical pair: aaabababcaaaabdaaaa=caaabbcbb.
Flip LHS and RHS.
Defines rule #21.