X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Finject.ma;h=ecb854b4a13a3900acefdacfe1366c5ce4b6763d;hb=637ff9311e16f1d58e03d873f84c354e1cf1e716;hp=0e9ffe09050f189530c2755c29a91e7ad1684506;hpb=b31ab31a99065295b91003a0df95dec817cee5de;p=helm.git

diff --git a/matita/matita/lib/turing/inject.ma b/matita/matita/lib/turing/inject.ma
index 0e9ffe090..ecb854b4a 100644
--- a/matita/matita/lib/turing/inject.ma
+++ b/matita/matita/lib/turing/inject.ma
@@ -30,9 +30,16 @@ lapply (trans sig M)  #trans #x lapply (trans x) * *
 #s #a #m % [ @s | % [ @a | @m ] ]
 qed.
 
-axiom current_chars_change_vec: ∀sig,n,v,a,i. i < S n →
+lemma current_chars_change_vec: ∀sig,n,v,a,i. i < S n →
    current_chars sig ? (change_vec ? (S n) v a i) =
    change_vec ? (S n)(current_chars ?? v) (current ? a) i.
+#sig #n #v #a #i #Hi @(eq_vec … (None ?)) #i0 #Hi0
+change with (vec_map ?????) in match (current_chars ???);
+<(nth_vec_map … (niltape ?))
+cases (decidable_eq_nat i i0) #Hii0
+[ >Hii0 >nth_change_vec // >nth_change_vec //
+| >nth_change_vec_neq // >nth_change_vec_neq // @nth_vec_map ]
+qed.
 
 lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n → 
   ∀M,v,s,a,sn,an,mn.