A0 A1 B0 B1 C0 C1 D0 D1 E0 E1 C1L E0R D0R H1L D1R A0L A1L B1R C0L E1R id=3470440 dm_2 List of the all shift rules: (sr0) *D>(+-)* -> *(+-)D>* (sr1) *(+-) *(+)* -> *(+)E>* (sr3) *(-+) *(-+)* -> *(-+)B>* Lemma: The following transactions are true for any k: (1) *(k|++) *(k|-+)(-+|k)* --> *-(k|++)E>* (2') *-E>(-+|k)-* --> *-(k|++)E>+* (2") *-(k|-+) *-E>(-+|k)+* (3) .E>(-+|k)+. --> .E>(-+|k+1)+. --------- Lemma proof (induction on length of sequences (xx|k) ): a) (1) and (2) are trivialy true for k=0. (2") is true for any k (it don't uses recursion). b) Let (1) and (2) are proved for k. (1)/k+1 proof; (1') proof: *++(k|++) *++(k|-+) *++ *-E>-(+-|k)-* repack --> *-E>(-+|k)--* (2')/k --> *-(k|++)E>+-* 2 steps --> *-(k|++)+ *-+(k|++) *-+(k|-+) *(k+1|-+)(-+|k)-+* <-- (2') proof begin (2)/k --> *-(k|++)E>-+* step --> *-(k|++) *-(k|-+) *- *+D>(+-|k)-+* sr0 --> *+(k|+-)D>-+* step --> *+(k|+-) *+ *-E>(-+|k)++* <-- (2") OK ! (2)/k --> *-(k|++)E>++* <-- (2') OK ! sr2; pack --> *-(k+1|++)E>* OK ! (3) proof: .--E>(-+|k)+-. (2)/k --> .--(k|++)E>+-. 2 steps --> .--(k|++)+ .--+(k|++) .--+(k|-+) .-(k+1|-+) .-E>(-+|k+1)+. OK ! Using the simple history below we see that the position .E>(-+)+. is reached at step 8. (3) applied to this position gaurantee infinitnes of this machine ! .E>(-+|2)+. is reached at step 39. .E>(-+|3)+. is reached at step 146. --------- Simple History: --------- 0: 0 .+#. 3: 1 B> .++^ 4: 2 D> .++-^ 5: 1 .=++. 9: -1 .+=++. 11: -1 .#++. 13: 1 E> .+#+. 14: 2 E> .++#. 15: 3 E> .+++^ 16: 2 .+-^ 19: 1 .++^ 21: 1 .+-#. 23: 3 E> .+-+^ 24: 2 .+#-+. 30: 0 B> .++=+. 31: 1 D> .++-#. 32: 2 B> .++-+^ 33: 3 D> .++-+-^ 34: 2 .=+-++. 40: -2 .+=+-++. 42: -2 .#+-++. 44: 0 E> .+#-++. 45: 1 E> .++=++. 46: 0 .=-++. 49: -1 .+=-++. 51: -1 .#-++. 53: 1 E> .+=++. 54: 0 .+#--++. 58: 0 B> .++=-++. 59: 1 D> .++-=++. 60: 0 .=++++. 64: -2 .+=++++. 66: -2 .#++++. 68: 0 E> .+#+++. 69: 1 E> .++#++. 70: 2 E> .+++#+. 71: 3 E> .++++#. 72: 4 E> .+++++^ 73: 3 .+++-^ 76: 2 .++++^ 78: 2 .+++-#. 80: 4 E> .+++-+^ 81: 3 .+-=+. 86: 0 .++=+. 88: 0 .+-#+. 90: 2 E> .+-+#. 91: 3 E> .+-++^ 92: 2 .+--^ 95: 1 .+-+^ 97: 1 .+--#. 99: 3 E> .+--+^ 100: 2 .++#. 104: 2 B> .+++^ 105: 3 D> .+++-^ 106: 2 .+-=++. 110: 0 .++=++. 112: 0 .+-#++. 114: 2 E> .+-+#+. 115: 3 E> .+-++#. 116: 4 E> .+-+++^ 117: 3 .+-+-^ 120: 2 .+-++^ 122: 2 .+-+-#. 124: 4 E> .+-+-+^ 125: 3 .+#-+-+. 133: -1 B> .++=+-+. 134: 0 D> .++-#-+. 135: 1 B> .++-+=+. 136: 2 D> .++-+-#. 137: 3 B> .++-+-+^ 138: 4 D> .++-+-+-^ 139: 3 .=+-+-++. 147: -3 .+=+-+-++. 149: -3 .#+-+-++. 151: -1 E> .+#-+-++. 152: 0 E> .++=+-++. 153: -1 .=-+-++. 156: -2 .+=-+-++. 158: -2 .#-+-++. 160: 0 E> .+=+-++. 161: -1 .+#--+-++. 165: -1 B> .++=-+-++. 166: 0 D> .++-=+-++. 167: -1 .=+++-++. 171: -3 .+=+++-++. 173: -3 .#+++-++. 175: -1 E> .+#++-++. 176: 0 E> .++#+-++. 177: 1 E> .+++#-++. 178: 2 E> .++++=++. 179: 1 .++-=-++. 182: 0 .+++=-++. 184: 0 .++-#-++. 186: 2 E> .++-+=++. 187: 1 .=+--++. 192: -2 .+=+--++. 194: -2 .#+--++. 196: 0 E> .+#--++. 197: 1 E> .++=-++. 198: 0 .=--++. 201: -1 .+=--++. 203: -1 .#--++. 205: 1 E> .+=-++. 206: 0 .+#---++. 210: 0 B> .++=--++. 211: 1 D> .++-=-++. 212: 0 .=++-++. 216: -2 .+=++-++. 218: -2 .#++-++. 220: 0 E> .+#+-++. 221: 1 E> .++#-++. 222: 2 E> .+++=++. 223: 1 .+-=-++. 226: 0 .++=-++. 228: 0 .+-#-++. 230: 2 E> .+-+=++. 231: 1 .+#-+--++. 237: -1 B> .++=+--++. 238: 0 D> .++-#--++. 239: 1 B> .++-+=-++. 240: 2 D> .++-+-=++. 241: 1 .=+-++++. 247: -3 .+=+-++++. 249: -3 .#+-++++. 251: -1 E> .+#-++++. 252: 0 E> .++=++++. 253: -1 .=-++++. 256: -2 .+=-++++. 258: -2 .#-++++. 260: 0 E> .+=++++. 261: -1 .+#--++++. 265: -1 B> .++=-++++. 266: 0 D> .++-=++++. 267: -1 .=++++++. 271: -3 .+=++++++. 273: -3 .#++++++. 275: -1 E> .+#+++++. 276: 0 E> .++#++++. 277: 1 E> .+++#+++. 278: 2 E> .++++#++. 279: 3 E> .+++++#+. 280: 4 E> .++++++#. 281: 5 E> .+++++++^ 282: 4 .+++++-^ 285: 3 .++++++^ 287: 3 .+++++-#. 289: 5 E> .+++++-+^ 290: 4 .+++-=+. 295: 1 .++++=+. 297: 1 .+++-#+. 299: 3 E> .+++-+#. 300: 4 E> .+++-++^ 301: 3 .+++--^ 304: 2 .+++-+^ 306: 2 .+++--#. 308: 4 E> .+++--+^ 309: 3 .++++#. 313: 3 B> .+++++^ 314: 4 D> .+++++-^ 315: 3 .+++-=++. 319: 1 .++++=++. 321: 1 .+++-#++. 323: 3 E> .+++-+#+. 324: 4 E> .+++-++#. 325: 5 E> .+++-+++^ 326: 4 .+++-+-^ 329: 3 .+++-++^ 331: 3 .+++-+-#. 333: 5 E> .+++-+-+^ 334: 4 .+-=+-+. 341: -1 .++=+-+. 343: -1 .+-#+-+. 345: 1 E> .+-+#-+. 346: 2 E> .+-++=+. 347: 1 .+--=-+. 350: 0 .+-+=-+. 352: 0 .+--#-+. 354: 2 E> .+--+=+. 355: 1 .++#--+. 359: 1 B> .+++=-+. 360: 2 D> .+++-=+. 361: 1 .+-=+++. 365: -1 .++=+++. 367: -1 .+-#+++. 369: 1 E> .+-+#++. 370: 2 E> .+-++#+. 371: 3 E> .+-+++#. 372: 4 E> .+-++++^ 373: 3 .+-++-^ 376: 2 .+-+++^ 378: 2 .+-++-#. 380: 4 E> .+-++-+^ 381: 3 .+--=+. 386: 0 .+-+=+. 388: 0 .+--#+. 390: 2 E> .+--+#. 391: 3 E> .+--++^ 392: 2 .+---^ 395: 1 .+--+^ 397: 1 .+---#. 399: 3 E> .+---+^ 400: 2