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)  *(+-)<A* -> *<A(-+)*  
(sr2)  *E>(+)*  -> *(+)E>*   
(sr3)  *(-+)<C* -> *<C(+-)*   
(sr4)  *B>(-+)* -> *(-+)B>*   

Lemma:

The following transactions are true for any k:

(1)  *(k|++)<C-*  --> *(k|-+)<C-*
(2)  *-E>(-+|k)*  --> *-(k|++)E>*
(2') *-E>(-+|k)-* --> *-(k|++)E>+*
(2") *-(k|-+)<C-* --> *-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|++)<C-*  
      (1)/k     -->  *++(k|-+)<C-*
      sr3       -->  *++<C(+-|k)-*
      2 steps   -->  *-E>-(+-|k)-*
      repack    -->  *-E>(-+|k)--*
      (2')/k    -->  *-(k|++)E>+-*
      2 steps   -->  *-(k|++)+<C-*
      repack    -->  *-+(k|++)<C-*
      (1)/k     -->  *-+(k|-+)<C-*
      pack      -->  *(k+1|-+)<C-*  OK !
      

   (2)/k+1 proof; (2') & (2") proof:  

                     *-E>(-+|k)-+*  <-- (2') proof begin
      (2)/k     -->  *-(k|++)E>-+*
      step      -->  *-(k|++)<C-+*
      (1)/k     -->  *-(k|-+)<C-+*  <-- (2") proof begin
      sr3       -->  *-<C(+-|k)-+*
      step      -->  *+D>(+-|k)-+*
      sr0       -->  *+(k|+-)D>-+*
      step      -->  *+(k|+-)<A++*
      sr1       -->  *+<A(-+|k)++*
      step      -->  *-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|++)+<C-.
      repack    -->  .--+(k|++)<C-.
      (1)/k     -->  .--+(k|-+)<C-.
      pack      -->  .-(k+1|-+)<C-.
      (2")/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 <A                    ^.
   1:   -1 <C                   ^+.
   2:    0 D>                  .+#.
   3:    1 B>                  .++^
   4:    2 D>                  .++-^
   5:    1 <A                  .++=+.
   6:    0 <C                  .+#++.
   7:   -1 <A                  .#-++.
   8:    0 E>                   .=++.
   9:   -1 <C                   ^-++.
  10:    0 D>                  .+=++.
  11:   -1 <A                  .#+++.
  12:    0 E>                   .#++.
  13:    1 E>                   .+#+.
  14:    2 E>                   .++#.
  15:    3 E>                   .+++^
  16:    2 <C                   .++#.
  17:    1 <A                   .+#.
  18:    2 E>                   .+-^
  19:    1 <C                   .+=.
  20:    2 D>                   .++^
  21:    1 <A                   .+#+.
  22:    2 E>                   .+-#.
  23:    3 E>                   .+-+^
  24:    2 <C                   .+-#.
  25:    1 <A                   .+=.
  26:    0 <C                   .#+.
  27:   -1 <A                   ^-+.
  28:   -2 <C                  ^+-+.
  29:   -1 D>                 .+#-+.
  30:    0 B>                 .++=+.
  31:    1 D>                 .++-#.
  32:    2 B>                 .++-+^
  33:    3 D>                 .++-+-^
  34:    2 <A                 .++-+=+.
  35:    1 <C                 .++-#++.
  36:    0 <A                 .++=-++.
  37:   -1 <C                 .+#+-++.
  38:   -2 <A                 .#-+-++.
  39:   -1 E>                  .=+-++.
  40:   -2 <C                  ^-+-++.
  41:   -1 D>                 .+=+-++.
  42:   -2 <A                 .#++-++.
  43:   -1 E>                  .#+-++.
  44:    0 E>                  .+#-++.
  45:    1 E>                  .++=++.
  46:    0 <C                  .+#-++.
  47:   -1 <A                  .#--++.
  48:    0 E>                   .=-++.
  49:   -1 <C                   ^--++.
  50:    0 D>                  .+=-++.
  51:   -1 <A                  .#+-++.
  52:    0 E>                   .#-++.
  53:    1 E>                   .+=++.
  54:    0 <C                   .#-++.
  55:   -1 <A                   ^--++.
  56:   -2 <C                  ^+--++.
  57:   -1 D>                 .+#--++.
  58:    0 B>                 .++=-++.
  59:    1 D>                 .++-=++.
  60:    0 <A                 .++=+++.
  61:   -1 <C                 .+#++++.
  62:   -2 <A                 .#-++++.
  63:   -1 E>                  .=++++.
  64:   -2 <C                  ^-++++.
  65:   -1 D>                 .+=++++.
  66:   -2 <A                 .#+++++.
  67:   -1 E>                  .#++++.
  68:    0 E>                  .+#+++.
  69:    1 E>                  .++#++.
  70:    2 E>                  .+++#+.
  71:    3 E>                  .++++#.
  72:    4 E>                  .+++++^
  73:    3 <C                  .++++#.
  74:    2 <A                  .+++#.
  75:    3 E>                  .+++-^
  76:    2 <C                  .+++=.
  77:    3 D>                  .++++^
  78:    2 <A                  .+++#+.
  79:    3 E>                  .+++-#.
  80:    4 E>                  .+++-+^
  81:    3 <C                  .+++-#.
  82:    2 <A                  .+++=.
  83:    1 <C                  .++#+.
  84:    0 <A                  .+#-+.
  85:    1 E>                  .+-=+.
  86:    0 <C                  .+=-+.
  87:    1 D>                  .++=+.
  88:    0 <A                  .+#++.
  89:    1 E>                  .+-#+.
  90:    2 E>                  .+-+#.
  91:    3 E>                  .+-++^
  92:    2 <C                  .+-+#.
  93:    1 <A                  .+-#.
  94:    2 E>                  .+--^
  95:    1 <C                  .+-=.
  96:    2 D>                  .+-+^
  97:    1 <A                  .+-#+.
  98:    2 E>                  .+--#.
  99:    3 E>                  .+--+^
 100:    2 <C                  .+--#.
 101:    1 <A                  .+-=.
 102:    0 <C                  .+=+.
 103:    1 D>                  .++#.
 104:    2 B>                  .+++^
 105:    3 D>                  .+++-^
 106:    2 <A                  .+++=+.
 107:    1 <C                  .++#++.
 108:    0 <A                  .+#-++.
 109:    1 E>                  .+-=++.
 110:    0 <C                  .+=-++.
 111:    1 D>                  .++=++.
 112:    0 <A                  .+#+++.
 113:    1 E>                  .+-#++.
 114:    2 E>                  .+-+#+.
 115:    3 E>                  .+-++#.
 116:    4 E>                  .+-+++^
 117:    3 <C                  .+-++#.
 118:    2 <A                  .+-+#.
 119:    3 E>                  .+-+-^
 120:    2 <C                  .+-+=.
 121:    3 D>                  .+-++^
 122:    2 <A                  .+-+#+.
 123:    3 E>                  .+-+-#.
 124:    4 E>                  .+-+-+^
 125:    3 <C                  .+-+-#.
 126:    2 <A                  .+-+=.
 127:    1 <C                  .+-#+.
 128:    0 <A                  .+=-+.
 129:   -1 <C                  .#+-+.
 130:   -2 <A                  ^-+-+.
 131:   -3 <C                 ^+-+-+.
 132:   -2 D>                .+#-+-+.
 133:   -1 B>                .++=+-+.
 134:    0 D>                .++-#-+.
 135:    1 B>                .++-+=+.
 136:    2 D>                .++-+-#.
 137:    3 B>                .++-+-+^
 138:    4 D>                .++-+-+-^
 139:    3 <A                .++-+-+=+.
 140:    2 <C                .++-+-#++.
 141:    1 <A                .++-+=-++.
 142:    0 <C                .++-#+-++.
 143:   -1 <A                .++=-+-++.
 144:   -2 <C                .+#+-+-++.
 145:   -3 <A                .#-+-+-++.
 146:   -2 E>                 .=+-+-++.
 147:   -3 <C                 ^-+-+-++.
 148:   -2 D>                .+=+-+-++.
 149:   -3 <A                .#++-+-++.
 150:   -2 E>                 .#+-+-++.
 151:   -1 E>                 .+#-+-++.
 152:    0 E>                 .++=+-++.
 153:   -1 <C                 .+#-+-++.
 154:   -2 <A                 .#--+-++.
 155:   -1 E>                  .=-+-++.
 156:   -2 <C                  ^--+-++.
 157:   -1 D>                 .+=-+-++.
 158:   -2 <A                 .#+-+-++.
 159:   -1 E>                  .#-+-++.
 160:    0 E>                  .+=+-++.
 161:   -1 <C                  .#-+-++.
 162:   -2 <A                  ^--+-++.
 163:   -3 <C                 ^+--+-++.
 164:   -2 D>                .+#--+-++.
 165:   -1 B>                .++=-+-++.
 166:    0 D>                .++-=+-++.
 167:   -1 <A                .++=++-++.
 168:   -2 <C                .+#+++-++.
 169:   -3 <A                .#-+++-++.
 170:   -2 E>                 .=+++-++.
 171:   -3 <C                 ^-+++-++.
 172:   -2 D>                .+=+++-++.
 173:   -3 <A                .#++++-++.
 174:   -2 E>                 .#+++-++.
 175:   -1 E>                 .+#++-++.
 176:    0 E>                 .++#+-++.
 177:    1 E>                 .+++#-++.
 178:    2 E>                 .++++=++.
 179:    1 <C                 .+++#-++.
 180:    0 <A                 .++#--++.
 181:    1 E>                 .++-=-++.
 182:    0 <C                 .++=--++.
 183:    1 D>                 .+++=-++.
 184:    0 <A                 .++#+-++.
 185:    1 E>                 .++-#-++.
 186:    2 E>                 .++-+=++.
 187:    1 <C                 .++-#-++.
 188:    0 <A                 .++=--++.
 189:   -1 <C                 .+#+--++.
 190:   -2 <A                 .#-+--++.
 191:   -1 E>                  .=+--++.
 192:   -2 <C                  ^-+--++.
 193:   -1 D>                 .+=+--++.
 194:   -2 <A                 .#++--++.
 195:   -1 E>                  .#+--++.
 196:    0 E>                  .+#--++.
 197:    1 E>                  .++=-++.
 198:    0 <C                  .+#--++.
 199:   -1 <A                  .#---++.
 200:    0 E>                   .=--++.
 201:   -1 <C                   ^---++.
 202:    0 D>                  .+=--++.
 203:   -1 <A                  .#+--++.
 204:    0 E>                   .#--++.
 205:    1 E>                   .+=-++.
 206:    0 <C                   .#--++.
 207:   -1 <A                   ^---++.
 208:   -2 <C                  ^+---++.
 209:   -1 D>                 .+#---++.
 210:    0 B>                 .++=--++.
 211:    1 D>                 .++-=-++.
 212:    0 <A                 .++=+-++.
 213:   -1 <C                 .+#++-++.
 214:   -2 <A                 .#-++-++.
 215:   -1 E>                  .=++-++.
 216:   -2 <C                  ^-++-++.
 217:   -1 D>                 .+=++-++.
 218:   -2 <A                 .#+++-++.
 219:   -1 E>                  .#++-++.
 220:    0 E>                  .+#+-++.
 221:    1 E>                  .++#-++.
 222:    2 E>                  .+++=++.
 223:    1 <C                  .++#-++.
 224:    0 <A                  .+#--++.
 225:    1 E>                  .+-=-++.
 226:    0 <C                  .+=--++.
 227:    1 D>                  .++=-++.
 228:    0 <A                  .+#+-++.
 229:    1 E>                  .+-#-++.
 230:    2 E>                  .+-+=++.
 231:    1 <C                  .+-#-++.
 232:    0 <A                  .+=--++.
 233:   -1 <C                  .#+--++.
 234:   -2 <A                  ^-+--++.
 235:   -3 <C                 ^+-+--++.
 236:   -2 D>                .+#-+--++.
 237:   -1 B>                .++=+--++.
 238:    0 D>                .++-#--++.
 239:    1 B>                .++-+=-++.
 240:    2 D>                .++-+-=++.
 241:    1 <A                .++-+=+++.
 242:    0 <C                .++-#++++.
 243:   -1 <A                .++=-++++.
 244:   -2 <C                .+#+-++++.
 245:   -3 <A                .#-+-++++.
 246:   -2 E>                 .=+-++++.
 247:   -3 <C                 ^-+-++++.
 248:   -2 D>                .+=+-++++.
 249:   -3 <A                .#++-++++.
 250:   -2 E>                 .#+-++++.
 251:   -1 E>                 .+#-++++.
 252:    0 E>                 .++=++++.
 253:   -1 <C                 .+#-++++.
 254:   -2 <A                 .#--++++.
 255:   -1 E>                  .=-++++.
 256:   -2 <C                  ^--++++.
 257:   -1 D>                 .+=-++++.
 258:   -2 <A                 .#+-++++.
 259:   -1 E>                  .#-++++.
 260:    0 E>                  .+=++++.
 261:   -1 <C                  .#-++++.
 262:   -2 <A                  ^--++++.
 263:   -3 <C                 ^+--++++.
 264:   -2 D>                .+#--++++.
 265:   -1 B>                .++=-++++.
 266:    0 D>                .++-=++++.
 267:   -1 <A                .++=+++++.
 268:   -2 <C                .+#++++++.
 269:   -3 <A                .#-++++++.
 270:   -2 E>                 .=++++++.
 271:   -3 <C                 ^-++++++.
 272:   -2 D>                .+=++++++.
 273:   -3 <A                .#+++++++.
 274:   -2 E>                 .#++++++.
 275:   -1 E>                 .+#+++++.
 276:    0 E>                 .++#++++.
 277:    1 E>                 .+++#+++.
 278:    2 E>                 .++++#++.
 279:    3 E>                 .+++++#+.
 280:    4 E>                 .++++++#.
 281:    5 E>                 .+++++++^
 282:    4 <C                 .++++++#.
 283:    3 <A                 .+++++#.
 284:    4 E>                 .+++++-^
 285:    3 <C                 .+++++=.
 286:    4 D>                 .++++++^
 287:    3 <A                 .+++++#+.
 288:    4 E>                 .+++++-#.
 289:    5 E>                 .+++++-+^
 290:    4 <C                 .+++++-#.
 291:    3 <A                 .+++++=.
 292:    2 <C                 .++++#+.
 293:    1 <A                 .+++#-+.
 294:    2 E>                 .+++-=+.
 295:    1 <C                 .+++=-+.
 296:    2 D>                 .++++=+.
 297:    1 <A                 .+++#++.
 298:    2 E>                 .+++-#+.
 299:    3 E>                 .+++-+#.
 300:    4 E>                 .+++-++^
 301:    3 <C                 .+++-+#.
 302:    2 <A                 .+++-#.
 303:    3 E>                 .+++--^
 304:    2 <C                 .+++-=.
 305:    3 D>                 .+++-+^
 306:    2 <A                 .+++-#+.
 307:    3 E>                 .+++--#.
 308:    4 E>                 .+++--+^
 309:    3 <C                 .+++--#.
 310:    2 <A                 .+++-=.
 311:    1 <C                 .+++=+.
 312:    2 D>                 .++++#.
 313:    3 B>                 .+++++^
 314:    4 D>                 .+++++-^
 315:    3 <A                 .+++++=+.
 316:    2 <C                 .++++#++.
 317:    1 <A                 .+++#-++.
 318:    2 E>                 .+++-=++.
 319:    1 <C                 .+++=-++.
 320:    2 D>                 .++++=++.
 321:    1 <A                 .+++#+++.
 322:    2 E>                 .+++-#++.
 323:    3 E>                 .+++-+#+.
 324:    4 E>                 .+++-++#.
 325:    5 E>                 .+++-+++^
 326:    4 <C                 .+++-++#.
 327:    3 <A                 .+++-+#.
 328:    4 E>                 .+++-+-^
 329:    3 <C                 .+++-+=.
 330:    4 D>                 .+++-++^
 331:    3 <A                 .+++-+#+.
 332:    4 E>                 .+++-+-#.
 333:    5 E>                 .+++-+-+^
 334:    4 <C                 .+++-+-#.
 335:    3 <A                 .+++-+=.
 336:    2 <C                 .+++-#+.
 337:    1 <A                 .+++=-+.
 338:    0 <C                 .++#+-+.
 339:   -1 <A                 .+#-+-+.
 340:    0 E>                 .+-=+-+.
 341:   -1 <C                 .+=-+-+.
 342:    0 D>                 .++=+-+.
 343:   -1 <A                 .+#++-+.
 344:    0 E>                 .+-#+-+.
 345:    1 E>                 .+-+#-+.
 346:    2 E>                 .+-++=+.
 347:    1 <C                 .+-+#-+.
 348:    0 <A                 .+-#--+.
 349:    1 E>                 .+--=-+.
 350:    0 <C                 .+-=--+.
 351:    1 D>                 .+-+=-+.
 352:    0 <A                 .+-#+-+.
 353:    1 E>                 .+--#-+.
 354:    2 E>                 .+--+=+.
 355:    1 <C                 .+--#-+.
 356:    0 <A                 .+-=--+.
 357:   -1 <C                 .+=+--+.
 358:    0 D>                 .++#--+.
 359:    1 B>                 .+++=-+.
 360:    2 D>                 .+++-=+.
 361:    1 <A                 .+++=++.
 362:    0 <C                 .++#+++.
 363:   -1 <A                 .+#-+++.
 364:    0 E>                 .+-=+++.
 365:   -1 <C                 .+=-+++.
 366:    0 D>                 .++=+++.
 367:   -1 <A                 .+#++++.
 368:    0 E>                 .+-#+++.
 369:    1 E>                 .+-+#++.
 370:    2 E>                 .+-++#+.
 371:    3 E>                 .+-+++#.
 372:    4 E>                 .+-++++^
 373:    3 <C                 .+-+++#.
 374:    2 <A                 .+-++#.
 375:    3 E>                 .+-++-^
 376:    2 <C                 .+-++=.
 377:    3 D>                 .+-+++^
 378:    2 <A                 .+-++#+.
 379:    3 E>                 .+-++-#.
 380:    4 E>                 .+-++-+^
 381:    3 <C                 .+-++-#.
 382:    2 <A                 .+-++=.
 383:    1 <C                 .+-+#+.
 384:    0 <A                 .+-#-+.
 385:    1 E>                 .+--=+.
 386:    0 <C                 .+-=-+.
 387:    1 D>                 .+-+=+.
 388:    0 <A                 .+-#++.
 389:    1 E>                 .+--#+.
 390:    2 E>                 .+--+#.
 391:    3 E>                 .+--++^
 392:    2 <C                 .+--+#.
 393:    1 <A                 .+--#.
 394:    2 E>                 .+---^
 395:    1 <C                 .+--=.
 396:    2 D>                 .+--+^
 397:    1 <A                 .+--#+.
 398:    2 E>                 .+---#.
 399:    3 E>                 .+---+^
 400:    2 <C                 .+---#.

-----------------------------------