sqrt.ma

[helm.git] / matita / matita / lib / turing / mono.ma

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 32bd28c87ffe0cfc65daa261c757f7c1fb831d93..d5fc9a187a29d7e0f75354f784a363db76b55872 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -292,6 +292,21 @@ lemma WRealize_to_GRealize : ∀sig.∀M: TM sig.∀Pre,R.
 @(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
 qed.
 
+lemma Realize_to_GRealize : ∀sig,M.∀P,R. 
+  M ⊨ R → GRealize sig M P R.
+#alpha #M #Pre #R #HR #t #HPre
+cases (HR t) -HR #k * #outc * #Hloop #HR 
+@(ex_intro ?? k) @(ex_intro ?? outc) % 
+  [ @Hloop | @HR ]
+qed.
+
+lemma acc_Realize_to_acc_GRealize: ∀sig,M.∀q:states sig M.∀P,R1,R2. 
+  M ⊨ [q:R1,R2] → accGRealize sig M q P R1 R2.
+#alpha #M #q #Pre #R1 #R2 #HR #t #HPre
+cases (HR t) -HR #k * #outc * * #Hloop #HRtrue #HRfalse 
+@(ex_intro ?? k) @(ex_intro ?? outc) % 
+  [ % [@Hloop] @HRtrue | @HRfalse]
+qed.
 
 (******************************** monotonicity ********************************)
 lemma Realize_to_Realize : ∀alpha,M,R1,R2.
@@ -314,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