A0 A1 B0 B1 C0 C1 D0 D1 E0 E1
C1L E1R D0R H1L D1R A0L A1L B1R E0R C0L id=3470230 dm_2
List of the shift rules:
(sr0) *D>(+-)* -> *(+-)D>*
(sr1) *(+-) *(-)* -> *(-)E>*
(sr3) *(-+) *(-+)* -> *(-+)B>*
Lemma:
The following transactions are true for any k:
(1) *(k|--) *(k|-+) .(k+1|-+) *+(k|-+)(-+|k)* --> *+(k|--)E>*
---------
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:
*--(k|--) *--(k|-+) *-+D>(+-|k)-*
sr0; step --> *-+(k|+-) *-+E>(-+|k)+*
(2)/k --> *-+(k|--)E>+*
step --> *-+(k|--) *-+(k|-+) *(k+1|-+)(-+|k)-+*
(2)/k --> *+(k|--)E>-+*
2 steps --> *+(k|--)- *+-(k|--) *++(k|-+) *++ *+E>-(+-|k)-*
repack --> *+E>(-+|k)--*
(2)/k --> *+(k|--)E>--*
sr2; pack --> *+(k+1|--)E>* OK!
Using the simple history below we see that the position .(2|-+) .+#.
3: 1 B> .++^
4: 2 D> .++-^
5: 1 .+=++.
9: 1 E> .+-#+.
10: 0 .++=+.
12: 0 .++#+.
14: 0 .+=-+.
17: 1 E> .+-=+.
18: 2 E> .+--#.
19: 1 .+-+^
21: 1 .+-+#.
23: 1 .+#-+.
29: -1 B> .++=+.
30: 0 D> .++-#.
31: 1 B> .++-+^
32: 2 D> .++-+-^
33: 1 .+=+-++.
39: -1 E> .+-#-++.
40: -2 .++=-++.
42: -2 .++#-++.
44: -2 .+=--++.
47: -1 E> .+-=-++.
48: 0 E> .+--=++.
49: 1 E> .+---#+.
50: 0 .+--+=+.
52: 0 .+--+#+.
54: 0 .++#--+.
58: 0 B> .+++=-+.
59: 1 D> .+++-=+.
60: 0 .++=+++.
64: 0 E> .++-#++.
65: -1 .+++=++.
67: -1 .+++#++.
69: -1 .++=-++.
72: 0 E> .++-=++.
73: 1 E> .++--#+.
74: 0 .++-+=+.
76: 0 .++-+#+.
78: 0 .+=+--+.
83: -1 E> .+-#--+.
84: -2 .++=--+.
86: -2 .++#--+.
88: -2 .+=---+.
91: -1 E> .+-=--+.
92: 0 E> .+--=-+.
93: 1 E> .+---=+.
94: 2 E> .+----#.
95: 1 .+---+^
97: 1 .+---+#.
99: 1 .+-+#.
103: 1 B> .+-++^
104: 2 D> .+-++-^
105: 1 .+-+=++.
109: 1 E> .+-+-#+.
110: 0 .+-++=+.
112: 0 .+-++#+.
114: 0 .+-+=-+.
117: 1 E> .+-+-=+.
118: 2 E> .+-+--#.
119: 1 .+-+-+^
121: 1 .+-+-+#.
123: 1 .+#-+-+.
131: -3 B> .++=+-+.
132: -2 D> .++-#-+.
133: -1 B> .++-+=+.
134: 0 D> .++-+-#.
135: 1 B> .++-+-+^
136: 2 D> .++-+-+-^
137: 1 .+=+-+-++.
145: -3 E> .+-#-+-++.
146: -4 .++=-+-++.
148: -4 .++#-+-++.
150: -4 .+=--+-++.
153: -3 E> .+-=-+-++.
154: -2 E> .+--=+-++.
155: -1 E> .+---#-++.
156: -2 .+--+=-++.
158: -2 .+--+#-++.
160: -2 .++#---++.
164: -2 B> .+++=--++.
165: -1 D> .+++-=-++.
166: -2 .++=++-++.
170: -2 E> .++-#+-++.
171: -3 .+++=+-++.
173: -3 .+++#+-++.
175: -3 .++=-+-++.
178: -2 E> .++-=+-++.
179: -1 E> .++--#-++.
180: -2 .++-+=-++.
182: -2 .++-+#-++.
184: -2 .+=+---++.
189: -3 E> .+-#---++.
190: -4 .++=---++.
192: -4 .++#---++.
194: -4 .+=----++.
197: -3 E> .+-=---++.
198: -2 E> .+--=--++.
199: -1 E> .+---=-++.
200: 0 E> .+----=++.
201: 1 E> .+-----#+.
202: 0 .+----+=+.
204: 0 .+----+#+.
206: 0 .+--+#--+.
210: 0 B> .+--++=-+.
211: 1 D> .+--++-=+.
212: 0 .+--+=+++.
216: 0 E> .+--+-#++.
217: -1 .+--++=++.
219: -1 .+--++#++.
221: -1 .+--+=-++.
224: 0 E> .+--+-=++.
225: 1 E> .+--+--#+.
226: 0 .+--+-+=+.
228: 0 .+--+-+#+.
230: 0 .++#-+--+.
236: -2 B> .+++=+--+.
237: -1 D> .+++-#--+.
238: 0 B> .+++-+=-+.
239: 1 D> .+++-+-=+.
240: 0 .++=+-+++.
246: -2 E> .++-#-+++.
247: -3 .+++=-+++.
249: -3 .+++#-+++.
251: -3 .++=--+++.
254: -2 E> .++-=-+++.
255: -1 E> .++--=+++.
256: 0 E> .++---#++.
257: -1 .++--+=++.
259: -1 .++--+#++.
261: -1 .+++#--++.
265: -1 B> .++++=-++.
266: 0 D> .++++-=++.
267: -1 .+++=++++.
271: -1 E> .+++-#+++.
272: -2 .++++=+++.
274: -2 .++++#+++.
276: -2 .+++=-+++.
279: -1 E> .+++-=+++.
280: 0 E> .+++--#++.
281: -1 .+++-+=++.
283: -1 .+++-+#++.
285: -1 .++=+--++.
290: -2 E> .++-#--++.
291: -3 .+++=--++.
293: -3 .+++#--++.
295: -3 .++=---++.
298: -2 E> .++-=--++.
299: -1 E> .++--=-++.
300: 0 E> .++---=++.
301: 1 E> .++----#+.
302: 0 .++---+=+.
304: 0 .++---+#+.
306: 0 .++-+#--+.
310: 0 B> .++-++=-+.
311: 1 D> .++-++-=+.
312: 0 .++-+=+++.
316: 0 E> .++-+-#++.
317: -1 .++-++=++.
319: -1 .++-++#++.
321: -1 .++-+=-++.
324: 0 E> .++-+-=++.
325: 1 E> .++-+--#+.
326: 0 .++-+-+=+.
328: 0 .++-+-+#+.
330: 0 .+=+-+--+.
337: -3 E> .+-#-+--+.
338: -4 .++=-+--+.
340: -4 .++#-+--+.
342: -4 .+=--+--+.
345: -3 E> .+-=-+--+.
346: -2 E> .+--=+--+.
347: -1 E> .+---#--+.
348: -2 .+--+=--+.
350: -2 .+--+#--+.
352: -2 .++#----+.
356: -2 B> .+++=---+.
357: -1 D> .+++-=--+.
358: -2 .++=++--+.
362: -2 E> .++-#+--+.
363: -3 .+++=+--+.
365: -3 .+++#+--+.
367: -3 .++=-+--+.
370: -2 E> .++-=+--+.
371: -1 E> .++--#--+.
372: -2 .++-+=--+.
374: -2 .++-+#--+.
376: -2 .+=+----+.
381: -3 E> .+-#----+.
382: -4 .++=----+.
384: -4 .++#----+.
386: -4 .+=-----+.
389: -3 E> .+-=----+.
390: -2 E> .+--=---+.
391: -1 E> .+---=--+.
392: 0 E> .+----=-+.
393: 1 E> .+-----=+.
394: 2 E> .+------#.
395: 1 .+-----+^
397: 1 .+-----+#.
399: 1