X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fmove_tape.ma;fp=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fmove_tape.ma;h=ab16d56c7f3c1a6af4c9b104a7437ccb26d845b4;hb=31cb2f0b374657eb5acb95708443e2c1b8481891;hp=ecc9fa2088840c1b80c2993151961f1a65315fc5;hpb=5af5db14a2bb7583ae1b8eaaf18ad26a06e3d892;p=helm.git

diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma
index ecc9fa208..ab16d56c7 100644
--- a/matita/matita/lib/turing/universal/move_tape.ma
+++ b/matita/matita/lib/turing/universal/move_tape.ma
@@ -626,13 +626,6 @@ cases (Hconcrete … Htable ? Ht1) //
       ] ] ] 
 | #x #Hx @Hbits @memb_append_l1 @Hx ]
 qed. 
-  
-lemma Realize_to_Realize : 
-  ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2.
-#alpha #M #R1 #R2 #Himpl #HR1 #intape
-cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
-@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
-qed.
 
 lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
 @(Realize_to_Realize … mtl_concrete_to_abstract) //