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