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)      *(+-)<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-*
(1') .(k|-+)<C.   --> .(k+1|-+)<C.
(1") *-(k|--)<C-* --> *+(k|-+)<C-*
(2)  *+E>(-+|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|--)<C-*  <-- (1") proof begin
      (1)/k     -->  *--(k|-+)<C-*  <-- (1') proof begin  
      sr3; step -->  *-+D>(+-|k)-*
      sr0; step -->  *-+(k|+-)<A+*
      sr1; step -->  *-+E>(-+|k)+*
      (2)/k     -->  *-+(k|--)E>+*
      step      -->  *-+(k|--)<C-*
      (1)/k     -->  *-+(k|-+)<C-*  <-- (1") OK!
      pack      -->  *(k+1|-+)<C-*  OK! <-- (1') OK!

   (2)/k+1 proof:
   
                     *+E>(-+|k)-+*
      (2)/k     -->  *+(k|--)E>-+*
      2 steps   -->  *+(k|--)-<C-*
      repack    -->  *+-(k|--)<C-*
      (1")/k    -->  *++(k|-+)<C-*
      sr3       -->  *++<C(+-|k)-*
      2 steps   -->  *+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|-+)<C.
is reached at step 23 (shorter notation is .+-+<C.) .
(1') applied to this position gaurantee infinitnes of this machine !

.(3|-+)<C. is reached at step 123.


Note: This proof is analog to proof_1375027.txt !


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

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