Changeset 3502

Timestamp:

Sep 25, 2014, 10:24:56 PM (5 years ago)

Author:

sacerdot

Message:

Tentative final statement and proof for Vm.ma.

File:

• LTS/Vm.ma (modified) (2 diffs)

LTS/Vm.ma

@@ -1105 +1105 @@
  ∀S: abstract_status. ∀s1,s2,s4 : S. raw_trace … s1 s4 → Prop ≝ 
 λS,s1,s2,s4,t.
+ pre_measurable_trace … t ∧
  ∃s3:S. ∃t' : raw_trace … s2 s3. ∃l1,l2,prf1,prf2.
   t = t_ind ? s1 s2 s4 l1 prf1 … (t' @ (t_ind ? s3 s4 s4 l2 prf2 … (t_base … s4)))
- ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ pre_measurable_trace … t.
+ ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2.
+
+(*
+lemma measurable_terminated:
+ ∀S,s1,s2,s4,t. measurable S s1 s2 s4 t → terminated_trace … t.
+ #S #s1 #s2 #s4 #t * #_ * #s3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct
+ /6 width=6 by ex_intro, conj/
+qed. *)
 
 theorem static_dynamic :
@@ -1139 +1147 @@
    applying every semantics in abs_trace. *) 
 R stn (〚abs_actions〛 a1).
+[2: @hide_prf cases daemon
+| #p #p' #prog #R #mT #map1 #EQmap #st0 #st1 #stn #t #measurable
+  cases measurable #premeas * #st3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct
+  #Hl1 #Hl2 #acts #EQacts #a1 #HR
+  cut (∃act.∃actstl. acts = act::actstl)
+  [ cases daemon (* usare measurable *) ]
+  * #act * #actstl #EQacts2 >EQacts2
+  cut (〚act::actstl〛 a1 = (〚actstl〛 (〚act〛 a1)))
+  [ cases daemon (* true *) ]
+  #EQ >EQ -EQ >EQacts2 in EQacts; #EQacts
+  @(static_dynamic_inv … EQmap … (t' @ t_ind … prf2 (t_base …)) … actstl … HR)
+  [ /6 width=6 by conj, ex_intro/
+  | cases daemon (* true *)
+  | cases daemon (* true *)
+  | cases daemon (* true *) ]]
+qed.