X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Finject.ma;h=d7851d85f938ba480045bd170c5e6c2f1a1af493;hb=2b51cf74b9a5f37d0f91780ceae4b8f4d0ee38a1;hp=be40c5638ce1ca95c233e4985ca8a906c3c29f8d;hpb=aa0fefefb9a2911739877f20897e00e16f7d3fd7;p=helm.git

diff --git a/matita/matita/lib/turing/inject.ma b/matita/matita/lib/turing/inject.ma
index be40c5638..d7851d85f 100644
--- a/matita/matita/lib/turing/inject.ma
+++ b/matita/matita/lib/turing/inject.ma
@@ -132,4 +132,22 @@ theorem sem_inject: ∀sig.∀M:TM sig.∀R.∀n,i.
     |#j #i >nth_change_vec_neq //
     ]
   ]
+qed.
+
+theorem acc_sem_inject: ∀sig.∀M:TM sig.∀Rtrue,Rfalse,acc.∀n,i.
+ i≤n → M ⊨ [ acc : Rtrue, Rfalse ] → 
+ inject_TM sig M n i ⊨ [ acc : inject_R sig Rtrue n i, inject_R sig Rfalse n i ]. 
+#sig #M #Rtrue #Rfalse #acc #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
+#k * * #outs #outt * * #Hloop #HRtrue #HRfalse @(ex_intro ?? k) 
+@(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) % [ %
+  [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
+   @loop_inject /2 by refl, trans_eq, le_S_S/
+  |#Hqtrue %
+    [>nth_change_vec /2 by le_S_S/
+    |#j #Hneq >nth_change_vec_neq //
+    ] ]
+  |#Hqfalse %
+    [>nth_change_vec /2 by le_S_S/ @HRfalse @Hqfalse
+    |#j #Hneq >nth_change_vec_neq //
+    ] ]
 qed.
\ No newline at end of file