Changeset 3502
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3501 r3502 1105 1105 ∀S: abstract_status. ∀s1,s2,s4 : S. raw_trace … s1 s4 → Prop ≝ 1106 1106 λS,s1,s2,s4,t. 1107 pre_measurable_trace … t ∧ 1107 1108 ∃s3:S. ∃t' : raw_trace … s2 s3. ∃l1,l2,prf1,prf2. 1108 1109 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 (* 1113 lemma 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/ 1117 qed. *) 1110 1118 1111 1119 theorem static_dynamic : … … 1139 1147 applying every semantics in abs_trace. *) 1140 1148 R 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 *) ]] 1164 qed.
Note: See TracChangeset
for help on using the changeset viewer.