progress in the deifinition of the semantics of the shift move.

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

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 27e81f5496c408354f8e4ad98f3af4b1dc792d87..3c6d686ea7b4f8359e53d2887df354917f32462c 100644 (file)
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -222,6 +222,20 @@ cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
   ]
 qed.
 
+lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc.
+  accRealize sig M1 acc Rtrue Rfalse  → M2 ⊨ R2  → M3 ⊨ R3 →  
+    (∀t1,t2,t3. (Rtrue t1 t3 ∧ R2 t3 t2) ∨ (Rfalse t1 t3 ∧ R3 t3 t2) → R4 t1 t2) → 
+    ifTM sig M1 M2 M3 acc ⊨ R4.
+#sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #R4 #acc
+#HRacc #HRtrue #HRfalse #Hsub
+#t cases (sem_if … HRacc HRtrue HRfalse t)
+#k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc)
+% [@Hloop] cases Houtc
+  [* #t3 * #Hleft #Hright @(Hsub … t3) %1 /2/
+  |* #t3 * #Hleft #Hright @(Hsub … t3) %2 /2/ ]
+qed.
+
+(* weak 
 lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc.
   accRealize sig M1 acc Rtrue Rfalse  → M2 ⊨ R2  → M3 ⊨ R3 →  
     (∀t1,t2,t3. (Rtrue t1 t3 → R2 t3 t2) ∨ (Rfalse t1 t3 → R3 t3 t2) → R4 t1 t2) → 
@@ -234,7 +248,8 @@ lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc.
   [* #t3 * #Hleft #Hright @(Hsub … t3) %1 /2/
   |* #t3 * #Hleft #Hright @(Hsub … t3) %2 /2/ ]
 qed.
- 
+*)
+
 (* we can probably use acc_sem_if to prove sem_if *)
 (* for sure we can use acc_sem_if_guarded to prove acc_sem_if *)
 lemma acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.