Changeset 3502 for LTS/Vm.ma


Ignore:
Timestamp:
Sep 25, 2014, 10:24:56 PM (5 years ago)
Author:
sacerdot
Message:

Tentative final statement and proof for Vm.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3501 r3502  
    11051105 ∀S: abstract_status. ∀s1,s2,s4 : S. raw_trace … s1 s4 → Prop ≝
    11061106λS,s1,s2,s4,t.
     1107 pre_measurable_trace … t ∧
    11071108 ∃s3:S. ∃t' : raw_trace … s2 s3. ∃l1,l2,prf1,prf2.
    11081109  t = t_ind ? s1 s2 s4 l1 prf1 … (t' @ (t_ind ? s3 s4 s4 l2 prf2 … (t_base … s4)))
    1109  ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ pre_measurable_trace … t.
     1110 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2.
     1111
     1112(*
     1113lemma measurable_terminated:
     1114 ∀S,s1,s2,s4,t. measurable S s1 s2 s4 t → terminated_trace … t.
     1115 #S #s1 #s2 #s4 #t * #_ * #s3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct
     1116 /6 width=6 by ex_intro, conj/
     1117qed. *)
    11101118
    11111119theorem static_dynamic :
     
    11391147   applying every semantics in abs_trace. *)
    11401148R stn (〚abs_actions〛 a1).
     1149[2: @hide_prf cases daemon
     1150| #p #p' #prog #R #mT #map1 #EQmap #st0 #st1 #stn #t #measurable
     1151  cases measurable #premeas * #st3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct
     1152  #Hl1 #Hl2 #acts #EQacts #a1 #HR
     1153  cut (∃act.∃actstl. acts = act::actstl)
     1154  [ cases daemon (* usare measurable *) ]
     1155  * #act * #actstl #EQacts2 >EQacts2
     1156  cut (〚act::actstl〛 a1 = (〚actstl〛 (〚act〛 a1)))
     1157  [ cases daemon (* true *) ]
     1158  #EQ >EQ -EQ >EQacts2 in EQacts; #EQacts
     1159  @(static_dynamic_inv … EQmap … (t' @ t_ind … prf2 (t_base …)) … actstl … HR)
     1160  [ /6 width=6 by conj, ex_intro/
     1161  | cases daemon (* true *)
     1162  | cases daemon (* true *)
     1163  | cases daemon (* true *) ]]
     1164qed.
Note: See TracChangeset for help on using the changeset viewer.