A0  A1   B0  B1   C0  C1   D0  D1   E0  E1
C1L D0R  C0L H1L  D1R B1L  A1R E1L  E0L A0R    id=1375027 dm_2

List of the shift rules:

(sr0)    *A>(+-)*  -->  *(-+)A>*
(sr1)    *(-+)<C*  -->  *<C(-+)*
(sr2)    *D>(-+)*  -->  *(+-)D>*
(sr3)    *(-)<E*   -->  *<E(-)*
(sr4)    *(+-)<B*  -->  *<B(+-)*

Lemma:

The following transactions are true for any k:

(1)  *-A>(--|k)*  --> *-A>(+-|k)*
(1') .A>(+-|k).   --> .A>(+-|k+1).
(1") *-A>(--|k)-* --> *-A>(+-|k)+*
(2)  *(k|+-)<E+*  --> *<E(--|k)+*

---------

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

   (2)/k+1 proof:

                     *+-(k|+-)<E+*
      (2)/k     -->  *+-<E(--|k)+*
      2 steps   -->  *-A>-(--|k)+*
      repack    -->  *-A>(--|k)-+*
      (1")/k    -->  *-A>(+-|k)++*
      sr0       -->  *-(k|-+)A>++*
      2 steps   -->  *-(k|-+)-<E+*
      repack    -->  *--(k|+-)<E+*
      (2)/k     -->  *--<E(--|k)+*
      sr3; pack -->  *<E(--|k+1)+*   OK!

Using the simple history below we see that the position .A>(+-|1).
is reached at step 4 (shorter notation is .A>+.). 
(1') applied to this position gaurantee infinitnes of this machine !

.A>(+-|2). is reached at step 28.
.A>(+-|3). is reached at step 128.

----- Simple History: -----
   0:    0 <A                                        ^.
   1:   -1 <C                                       ^+.
   2:    0 D>                                      .+#.
   3:   -1 <E                                      .#+.
   4:    0 A>                                       .#.
   5:    1 D>                                        .^
   6:    2 A>                                        .+^
   7:    1 <C                                        .#+.
   8:    0 <B                                        ^++.
   9:   -1 <C                                       ^-++.
  10:    0 D>                                      .+=++.
  11:    1 A>                                      .++#+.
  12:    2 D>                                      .++-#.
  13:    1 <E                                      .++=+.
  14:    0 <E                                      .+#-+.
  15:    1 A>                                      .+-=+.
  16:    0 <C                                      .+=++.
  17:    1 D>                                      .++#+.
  18:    0 <E                                      .+#++.
  19:    1 A>                                      .+-#+.
  20:    2 D>                                      .+--#.
  21:    1 <E                                      .+-=+.
  22:    0 <E                                      .+=-+.
  23:   -1 <E                                      .#--+.
  24:    0 A>                                       .=-+.
  25:   -1 <C                                       ^+-+.
  26:    0 D>                                      .+#-+.
  27:   -1 <E                                      .#+-+.
  28:    0 A>                                       .#-+.
  29:    1 D>                                        .=+.
  30:    2 A>                                        .+#.
  31:    3 D>                                        .+-^
  32:    4 A>                                        .+-+^
  33:    3 <C                                        .+-#+.
  34:    2 <B                                        .+=++.
  35:    1 <C                                        .#-++.
  36:    0 <B                                        ^+-++.
  37:   -1 <C                                       ^-+-++.
  38:    0 D>                                      .+=+-++.
  39:    1 A>                                      .++#-++.
  40:    2 D>                                      .++-=++.
  41:    3 A>                                      .++-+#+.
  42:    4 D>                                      .++-+-#.
  43:    3 <E                                      .++-+=+.
  44:    2 <E                                      .++-#-+.
  45:    3 A>                                      .++--=+.
  46:    2 <C                                      .++-=++.
  47:    3 D>                                      .++-+#+.
  48:    2 <E                                      .++-#++.
  49:    3 A>                                      .++--#+.
  50:    4 D>                                      .++---#.
  51:    3 <E                                      .++--=+.
  52:    2 <E                                      .++-=-+.
  53:    1 <E                                      .++=--+.
  54:    0 <E                                      .+#---+.
  55:    1 A>                                      .+-=--+.
  56:    0 <C                                      .+=+--+.
  57:    1 D>                                      .++#--+.
  58:    0 <E                                      .+#+--+.
  59:    1 A>                                      .+-#--+.
  60:    2 D>                                      .+--=-+.
  61:    3 A>                                      .+--+=+.
  62:    2 <C                                      .+--#++.
  63:    1 <B                                      .+-=+++.
  64:    0 <C                                      .+=-+++.
  65:    1 D>                                      .++=+++.
  66:    2 A>                                      .+++#++.
  67:    3 D>                                      .+++-#+.
  68:    2 <E                                      .+++=++.
  69:    1 <E                                      .++#-++.
  70:    2 A>                                      .++-=++.
  71:    1 <C                                      .++=+++.
  72:    2 D>                                      .+++#++.
  73:    1 <E                                      .++#+++.
  74:    2 A>                                      .++-#++.
  75:    3 D>                                      .++--#+.
  76:    2 <E                                      .++-=++.
  77:    1 <E                                      .++=-++.
  78:    0 <E                                      .+#--++.
  79:    1 A>                                      .+-=-++.
  80:    0 <C                                      .+=+-++.
  81:    1 D>                                      .++#-++.
  82:    0 <E                                      .+#+-++.
  83:    1 A>                                      .+-#-++.
  84:    2 D>                                      .+--=++.
  85:    3 A>                                      .+--+#+.
  86:    4 D>                                      .+--+-#.
  87:    3 <E                                      .+--+=+.
  88:    2 <E                                      .+--#-+.
  89:    3 A>                                      .+---=+.
  90:    2 <C                                      .+--=++.
  91:    3 D>                                      .+--+#+.
  92:    2 <E                                      .+--#++.
  93:    3 A>                                      .+---#+.
  94:    4 D>                                      .+----#.
  95:    3 <E                                      .+---=+.
  96:    2 <E                                      .+--=-+.
  97:    1 <E                                      .+-=--+.
  98:    0 <E                                      .+=---+.
  99:   -1 <E                                      .#----+.