X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmono.ma;h=d5fc9a187a29d7e0f75354f784a363db76b55872;hb=11daf1ea77fb51f8c9218957b2b912d4dbdc662a;hp=37ce2f2dee192414fc174a9783f0fd0fe4a5dd89;hpb=5535cd4e08fd8d1e7e6e067eac1bb6c1bf8fcbbf;p=helm.git

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 37ce2f2de..d5fc9a187 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -329,6 +329,13 @@ cases (HR1 intape HP) -HR1 #k * #outc * #Hloop #HR1
 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
 qed.
 
+lemma GRealize_to_GRealize_2 : ∀alpha,M,P1,P2,R1,R2.
+  P2 ⊆ P1 → R1 ⊆ R2 → GRealize alpha M P1 R1 → GRealize alpha M P2 R2.
+#alpha #M #P1 #P2 #R1 #R2 #Himpl1 #Himpl2 #H1 #intape #HP
+cases (H1 intape (Himpl1 … HP)) -H1 #k * #outc * #Hloop #H1
+@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
+qed.
+
 lemma acc_Realize_to_acc_Realize: ∀sig,M.∀q:states sig M.∀R1,R2,R3,R4. 
   R1 ⊆ R3 → R2 ⊆ R4 → M ⊨ [q:R1,R2] → M ⊨ [q:R3,R4].
 #alpha #M #q #R1 #R2 #R3 #R4 #Hsub13 #Hsub24 #HRa #intape