X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Fmoves.ma;h=f725a1940202b8bf641152ce2eeb21d433e5f98d;hb=53273ac4ac4e742f8767fc1f9ef0f279c0b80a1d;hp=df620b3520d63f5076a24be061661e7717201fe6;hpb=b31ab31a99065295b91003a0df95dec817cee5de;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/moves.ma b/matita/matita/lib/turing/multi_universal/moves.ma
index df620b352..f725a1940 100644
--- a/matita/matita/lib/turing/multi_universal/moves.ma
+++ b/matita/matita/lib/turing/multi_universal/moves.ma
@@ -159,14 +159,12 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
 [ #Hcursrc %{2} %
   [| % [ %
     [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/
-      <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
     | normalize in ⊢ (%→?); #H destruct (H) ]
     | #_ % // % %2 // ] ]
 | #a #Ha cases (true_or_false (is_sep a)) #Hsep
   [ %{2} %
     [| % [ %
       [ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/
-        <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
       | normalize in ⊢ (%→?); #H destruct (H) ]
       | #_ % // % % %{a} % // ] ]
   | lapply (refl ? (current ? (nth dst ? int (niltape ?))))
@@ -174,15 +172,11 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
     [ #Hcurdst %{2} %
       [| % [ %
         [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst … Hsep) /2/ 
-          [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
-          | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
         | normalize in ⊢ (%→?); #H destruct (H) ]
         | #_ % // %2 // ] ]
     | #b #Hb %{2} %
       [| % [ % 
         [whd in ⊢  (??%?);  >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ?? Hsep) //
-          [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
-          | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
         | #_ %{a} %{b} % // % // % // ]
         | * #H @False_ind @H % ]
 ]]]]