A0 A1 B0 B1 C0 C1 D0 D1 E0 E1 B1L H1L C1R A0L E1L D1R C0R B0L D0R E0L id=764350 dm_1 List of the shift rules: (sr0) *C>(+-)* --> *(+-)C>* (sr1) *(+) *(-+)* --> *(-+)D>* (sr3) *(-+) * *(--|k)* --> *-D>(-+|k)* (1') .D>(-+|k). --> .D>(-+|k+1). (2) *(k|-+)D>--* --> *(k|++)D>--* --------- Lemma proof (induction on length of sequences (xx|k) ): a) (1) and (2) are trivialy true for k=0. b) Let (1) and (2) are proved for k. (1)/k+1 proof; (1') proof: *-D>(--|k+1)* -- unpack --> *-D>(--|k)--* -- (1)/k --> *-D>(-+|k)--* <-- (1') proof begin -- sr2 --> *-(k|-+)D>--* -- (2)/k --> *-(k|++)D>--* -- steps --> *-(k|++) *- *-D>(--|k)-+* -- (1)/k --> *-D>(-+|k)-+* -- pack --> *-D>(-+|k+1)* OK! <-- (1') OK! (2)/k+1 proof: *(k+1|-+)D>--* -- unpack --> *-+(k|-+)D>--* -- (2)/k --> *-+(k|++)D>--* -- steps --> *-+(k|++) *- *- *-D>(--|k+1)+* -- (1)/k+1--> *-D>(-+|k+1)+* -- sr2 --> *-(k+1|-+)D>+* -- step --> *-(k+1|-+) *- *+C>(+-|k+1)-* -- unpack --> *+C>+-(+-|k)-* -- step --> *++D>-(+-|k)-* -- repack --> *++D>(-+|k)--* -- sr2 --> *++(k|-+)D>--* -- (2)/k --> *++(k|++)D>--* -- pack --> *(k+1|++)D>--* OK! Using the simple history below we see that the position .D>-+-+. is reached at step 21. (1') applied to this position gaurantee infinitnes of this machine ! Position .D>(-+|3). is reached at step 213 ! ----- Simple History: ----- 0: 0 .+#. 3: 1 D> .++^ 4: 2 C> .++-^ 5: 1 .++-#. 7: 1 .+++^ 9: 1 .=--+. 14: 0 C> .=-+. 15: -1 .#-+. 17: -1 .+=-+. 19: -1 .=+-+. 22: 0 C> .#-+. 23: 1 D> .+=+. 24: 2 C> .+-#. 25: 3 D> .+-+^ 26: 4 C> .+-+-^ 27: 3 .+-+-#. 29: 3 .+-++^ 31: 3 .+-=-+. 35: 3 C> .+--=+. 36: 2 .+--#+. 38: 2 .+-+=+. 40: 2 .+-=++. 43: 3 C> .+--#+. 44: 4 D> .+--+#. 45: 3 .++#. 49: 3 D> .+++^ 50: 4 C> .+++-^ 51: 3 .+++-#. 53: 3 .++++^ 55: 3 .=---+. 61: 1 C> .=--+. 62: 0 .#--+. 64: 0 .+=--+. 66: 0 .=+--+. 69: 1 C> .#--+. 70: 2 D> .+=-+. 71: 3 C> .+-=+. 72: 2 .+-#+. 74: 2 .++=+. 76: 2 .=-++. 80: 2 C> .=++. 81: 1 .#++. 83: 1 .+=++. 85: 1 .=+++. 88: 2 C> .#++. 89: 3 D> .+#+. 90: 2 .+#--+. 94: 2 D> .++=-+. 95: 3 C> .++-=+. 96: 2 .++-#+. 98: 2 .+++=+. 100: 2 .=--++. 105: 1 C> .=-++. 106: 0 .#-++. 108: 0 .+=-++. 110: 0 .=+-++. 113: 1 C> .#-++. 114: 2 D> .+=++. 115: 3 C> .+-#+. 116: 4 D> .+-+#. 117: 3 .+#-+. 123: 1 D> .++=+. 124: 2 C> .++-#. 125: 3 D> .++-+^ 126: 4 C> .++-+-^ 127: 3 .++-+-#. 129: 3 .++-++^ 131: 3 .++-=-+. 135: 3 C> .++--=+. 136: 2 .++--#+. 138: 2 .++-+=+. 140: 2 .++-=++. 143: 3 C> .++--#+. 144: 4 D> .++--+#. 145: 3 .+++#. 149: 3 D> .++++^ ------------------------------------------------------------