Changeset 3523 for LTS/Final.ma
 Timestamp:
 Mar 11, 2015, 12:59:28 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Final.ma
r3511 r3523 16 16 include "Vm.ma". 17 17 18 axiom simulates_measurable: 18 inductive no_io_trace (S : abstract_status) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝ 19 t_base_io :∀st : S.as_classify … st ≠ cl_io → no_io_trace S … (t_base … st) 20  t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io → 21 no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl). 22 23 lemma no_io_append : ∀S : abstract_status. 24 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2. 25 ∀t2 : raw_trace … st2 st3. 26 no_io_trace … t1 → no_io_trace … t2 → 27 no_io_trace … (t1 @ t2). 28 #S #st1 #st2 #st3 #t1 lapply st3 elim t1 29 [ #st #st3 #t2 #_ //] 30 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?; 31 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct ] 32 #st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #_ destruct 33 #H3 %2 // @IH // 34 qed. 35 36 lemma pre_measurable_no_io : ∀S : abstract_status. 37 ∀st1,st2 : S. ∀t : raw_trace … st1 st2. 38 pre_measurable_trace … t → 39 no_io_trace … t. 40 #S #st1 #st2 #t #H elim H /2/ st1st2 41 #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5 42 #H6 #IH1 #IH2 %2 // @no_io_append // %2 // 43 qed. 44 45 lemma head_of_no_io_is_no_io : ∀S : abstract_status. 46 ∀st1,st2 : S. ∀t : raw_trace … st1 st2. 47 no_io_trace … t → as_classify … st1 ≠ cl_io. 48 #S #st1 #st2 #t #H elim H // 49 qed. 50 51 52 lemma no_io_append_l1 : ∀S : abstract_status. 53 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2. 54 ∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) → 55 no_io_trace … t1. 56 #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/] 57 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?; 58 [ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ] 59 #st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct 60 %2 // @IH // 61 qed. 62 63 lemma no_io_append_l2 : ∀S : abstract_status. 64 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2. 65 ∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) → 66 no_io_trace … t2. 67 #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ] 68 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?; 69 [ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ] 70 #st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct // 71 qed. 72 73 lemma is_costlabelled_act_elim : 74 ∀P : ActionLabel → Prop. 75 (∀l. is_costlabelled_act l → P l) → 76 (∀l. ¬is_costlabelled_act l → P l) → 77 ∀l.P l. 78 #P #H1 #H2 * /2/ 79 [ * /2/ @H2 % *] * /2/ @H2 %* 80 qed. 81 82 (* 83 lemma append_silent_premeasurable_l : ∀S : abstract_status. 84 ∀st1,st2,st3,st4 : S.∀t1 : raw_trace … st1 st2.∀l,prf. 85 ∀t2 : raw_trace … st3 st4. 86 pre_measurable_trace … (t1 @ (t_ind … l prf t2)) → 87 as_classify … st2 ≠ cl_io. 88 #S #st1 #st2 #st3 #st4 #t1 lapply st4 lapply st3 st3 st4 elim t1 89 [ #st #st3 #st4 #l #prf #t2 #H @(head_of_premeasurable_is_not_io … H) 90  #st' #st'' #st''' #l1 #prf #tl #IH 91 *) 92 93 definition measurable_prefix ≝ 94 λS : abstract_status. 95 λs1,s4 :S. 96 λt : raw_trace … s1 s4. 97 ∃s2,s3 : S.∃t12 : raw_trace … s1 s2. 98 ∃l.∃prf : as_execute … l s2 s3. 99 ∃t34 : raw_trace … s3 s4. 100 silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l. 101 102 lemma measurable_prefix_of_premeasurable : 103 ∀S : abstract_status. 104 ∀s1,s4 : S. 105 ∀t : raw_trace … s1 s4. 106 pre_measurable_trace … t → 107 get_costlabels_of_trace … t ≠ nil ? → 108 measurable_prefix … t. 109 #S #s1 #s4 #t elim t 110 [ #st #_ * #H @⊥ @H %] 111 #st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) l 112 [ #l #Hl #prf #t' #IH #_ #_ %{st1} %{st2} %{(t_base …)} %{l} %{prf} %{t'} 113 % // % // %2 normalize % *] 114 #l #Hl #prf #t' #IH #H inversion H 115 [ #st #H1 #H2 #H3 #H4 #H5 destruct 116  #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 117 cases l2 in Hl Hl2 prf2; 118 [ #f #c #_ * #z #EQ destruct 119  * [#lbl] #_ * #z #EQ destruct 120  * [#lbl * #H cases(H I)] 121 ] 122  #x1 #x2 #x3 #l2 #Hclass #prf2 #tl #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 123 cases l2 in Hl Hl2 prf2; 124 [ #f #c #_ * #z #EQ destruct 125  #lbl1 #H1 * #z #EQ destruct cases H1 H1 #H1 @⊥ @H1 % 126  #lbl #_ * #z #EQ destruct 127 ] 128  #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #Hpost #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 129 cases l2 in Hl Hl2 prf2; 130 [ #f #c * #H @⊥ @H % 131  #lbl1 #_ * #z * #z1 #EQ destruct 132  #lbl #_ * #z * #z1 #EQ destruct 133 ] 134  #x1 #x2 #x3 #x4 #x5 #l2 #l3 #prf2 #tl1 #tl2 #prf3 #Hclass1 #Hclass2 #Hl2 #Hx1 #pre1 #pre2 #succ #Hl3 135 #_ #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 136 cases l2 in Hl Hl2 prf2; 137 [ #f #c * #H @⊥ @H % 138  #lbl1 #_ * #z * #z1 #EQ destruct 139  #lbl #_ * #z * #z1 #EQ destruct 140 ] 141 ] 142 #_ #_ #prf #H1 cases(IH pre_tl ?) 143 [2: % #EQ whd in H1 : (?(??%?)); >EQ in H1; * #H @H % ] 144 #s2 * #s3 * #t12 * #l1 * #prf1 * #t34 ** #H2 #H3 #H4 %{s2} %{s3} %{(t_ind … prf t12)} 145 %{l1} %{prf1} %{t34} % // % 146 [ % %2 // cases H2 // inversion t12 [2: #z1 #z2 #z3 #lbl #prf5 #tl1 #_ #EQ1 #EQ2 #E3 destruct * #H @⊥ @H // ] 147 #st #EQ1 #EQ2 #EQ3 destruct #_ % /2 by head_of_premeasurable_is_not_io/ 148  >H3 // 149 ] 150 qed. 151 152 (* 153 definition measurable_suffix ≝ 154 λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'. 155 ∃s1_em1 : S. 156 ∃t_pre_em : raw_trace … s1 s1_em1. 157 ∃s1_postem1 : S. 158 ∃t_post_em : raw_trace … s1_postem s1'. 159 silent_trace S ?? t_post_em ∧ 160 ∃l_em : ActionLabel. 161 ∃ex_em : as_execute … l_em s1_em s1_postem. 162 t = t_pre_em @ (t_ind … ex_em t_post_em) ∧ 163 (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)). 164 *) 165 166 lemma append_nil_is_nil : ∀S : abstract_status. 167 ∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1. 168 t1 @ t2 = t_base … s1 → s1 = s2 ∧ t1 ≃ t_base … s1 ∧ t2 ≃ t_base … s1. 169 #S #s1 #s2 #t1 elim t1 t1 s1 s2 170 [ #st #t2 normalize #EQ destruct /3 by refl_jmeq, conj/] 171 #s1 #s2 #s3 #l #prf #t2 #IH #t2 normalize #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 172 qed. 173 174 lemma append_silent : ∀S : abstract_status. 175 ∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2. 176 ∀t2 : raw_trace … s2 s3.silent_trace … t1 → 177 silent_trace … t2 → 178 silent_trace … (t1 @ t2). 179 #S #s1 #s2 #s3 #t1 elim t1 t1 s1 s2 180 [ #st #t2 #_ * /2 by or_introl, or_intror/ ] 181 #st1 #st2 #st3 #l #prf #tl #IH #t2 * 182 [2: * #H cases(H I) ] #H inversion H in ⊢ ?; 183 [ #st #H1 #H2 #H3 #H4 #H5 #H6 destruct ] 184 #st1' #st2' #st3' #prf' #tl' #Hst1' #Htl' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 185 #Ht2 % %2 // cases(IH … Ht2) /2/ 186 inversion(tl' @ t2) 187 [2: #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 * #H cases (H I) ] 188 #st #EQ1 #EQ2 destruct #H cases(append_nil_is_nil … H) * #EQ1 #EQ2 #EQ3 destruct // 189 qed. 190 191 192 definition measurable_suffix ≝ 193 λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'. 194 ∃s1_em : S. 195 ∃t_pre_em : raw_trace … s1 s1_em. 196 ∃s1_postem : S. 197 ∃t_post_em : raw_trace … s1_postem s1'. 198 silent_trace S ?? t_post_em ∧ 199 ∃l_em : ActionLabel. 200 ∃ex_em : as_execute … l_em s1_em s1_postem. 201 t = t_pre_em @ (t_ind … ex_em t_post_em) ∧ 202 (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧ 203 is_costlabelled_act l_em. 204 205 206 lemma measurable_suffix_tind : ∀S : abstract_status. 207 ∀s1,s2,s3 : S.∀l : ActionLabel.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3. 208 measurable_suffix … (t_ind … prf t) → (is_costlabelled_act l \wedge silent_trace … t) ∨ measurable_suffix … t. 209 #S #s1 #s2 #s3 #l #prf #t lapply prf prf lapply s1 s1 cases t t s2 s3 210 [ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em ** 211 inversion t_pre in ⊢ ?; 212 [#st' #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 213 #_ /4 by or_introl, conj/ 214  #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct normalize in H34; 215 lapply(eq_to_jmeq ??? H34) H34 #H34 destruct inversion H29 in ⊢ ?; 216 [ #H38 #H39 #H40 #H41 destruct 217  #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 destruct normalize in e1; destruct 218 ] 219 normalize in e0; destruct 220 ] 221 ] 222 #s1 #s2 #s3 #l1 #prf1 #tl #s4 #prf * #s_em * #t_post lapply prf prf cases t_post t_post 223 [ #s5 #prf * #s_post * #t_post * #sil_tpost * #l_em * #prf2 ** #EQ normalize in EQ; 224 lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct /4/ 225  #s5 #s6 #s7 #lbl #prf2 #tl1 #prf3 * #s_post * #t_post * #sil_tpost * #l_em * #ex_em ** 226 #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hcall #Hcost %2 227 >e0 whd %{s7} %{tl1} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/ 228 ] 229 qed. 230 231 lemma measurable_suffix_append : ∀S : abstract_status. 232 ∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 233 measurable_suffix … t2 → measurable_suffix … (t1 @ t2). 234 #S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post 235 * #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost 236 %{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/ 237 qed. 238 239 lemma silent_append_l2 : ∀S : abstract_status. 240 ∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 241 silent_trace … (t1 @ t2) → silent_trace … t2. 242 #S #s1 #s2 #s3 #t1 elim t1 // s1 s2 243 #st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] 244 #H @IH % inversion H in ⊢ ?; 245 [ #H42 #H43 #H44 #H45 normalize #H46 #H47 destruct 246  #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 normalize in H59; destruct assumption 247 ] 248 qed. 249 250 lemma silent_append_l1 : ∀S : abstract_status. 251 ∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 252 silent_trace … (t1 @ t2) → silent_trace … t1. 253 #S #s1 #s2 #s3 #t1 elim t1 s1 s2 254 [ #st #t2 #_ %2 % *] 255 #st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H 256 % inversion H in ⊢ ?; [ #H62 #H63 #H64 #H65 #H66 #H67 normalize in H66; destruct] 257 #z1 #z2 #z3 #prf' #tl' #Hclass #Htl' #_ #EQ1 #EQ2 #EQ3 normalize in EQ3; #EQ4 destruct 258 %2 // cases(IH t2 …) /2/ inversion tl 259 [2: #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct cases H79 #H cases(H I) ] 260 #st #EQ1 #EQ2 #EQ3 destruct #_ % normalize in Htl'; inversion Htl' 261 [ #H81 #H82 #H83 #H84 #H85 #H86 destruct // 262  #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct // 263 ] 264 qed. 265 266 lemma measurable_suffix_append_l1 : ∀S : abstract_status. 267 ∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 268 measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1. 269 #S #s1 #s2 #s3 #t1 elim t1 t1 s1 s2 270 [#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct 271 #Hcall #Hcost #H lapply(silent_append_l2 … H) H * [2: * #H cases(H I)] #H inversion H 272 [ #H113 #H114 #H115 #H116 #H117 #H118 destruct ] 273 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 destruct cases Hcost 274 ] 275 #st1 #st2 #st3 #l #prf #tl #IH #t2 * #s_em * #t_pre inversion t_pre in ⊢ ?; 276 [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em 277 * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 278 #Hcall #Hcost #sil_t2 %{st} %{(t_base …)} %{s_post} %{tl} % [ /2 by silent_append_l1/] 279 %{l_em} %{ex_em} /4 by refl, conj/ 280  #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em 281 ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hcall #Hcost #H 282 change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append @(IH t2) // 283 %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption 284 ] 285 qed. 286 287 lemma measurable_suffix_append_case : ∀S : abstract_status. 288 ∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 289 measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2. 290 #S #s1 #s2 #s3 #t1 elim t1 s1 s2 291 [ #st #t2 #H %2 assumption] 292 #st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff 293 cases(measurable_suffix_tind … Hsuff) 294 [ * #_ #H %% [2: /2 by silent_append_l2/] change with ((t_ind ?????? tl) @ t2) in Hsuff : (????%); 295 @(measurable_suffix_append_l1 … Hsuff) /2/ 296  #H cases(IH … H) 297 [ * #H1 #H2 %% // change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append // 298  /2/ 299 ] 300 ] 301 qed. 302 303 304 305 theorem simulates_pre_mesurable: 306 ∀S1,S2 : abstract_status.∀rel : relations S1 S2. 307 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'. 308 simulation_conditions … rel → 309 pre_measurable_trace … t1 → 310 ∀s2 : S2. 311 as_classify … s2 ≠ cl_io → Srel … rel s1 s2 → 312 ∃s2'. ∃t2: raw_trace … s2 s2'. 313 pre_measurable_trace … t2 ∧ 314 get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ 315 Srel … rel s1' s2' ∧ 316 (measurable_suffix … t1 → measurable_suffix … t2) ∧ 317 (silent_trace … t1 → silent_trace … t2). 318 #S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H t1 s1 s1' 319 [ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} % 320 [ % [ % // % // % //] * #s_em ** [ #sx  #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost 321 * #prf1 ** normalize #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 322  #_ %2 % * 323 ] 324  #st1 #st2 #st3 #l #prf #tl #Hclass ** 325 [ #EQ destruct #pre_tl #IH #s2 #Hclass2 #R_st1_s2 326 cases(simulate_tau … sim … prf … R_st1_s2) [2,3: /2 by head_of_premeasurable_is_not_io/] 327 #s2' * #t2_init * #R_st2_s2' #silent_t2_init cases(IH … R_st2_s2') 328 [2: cases silent_t2_init /2 by pre_silent_io/ cases t2_init in Hclass2; // 329 #H12 #H13 #H14 #H15 #H16 #H17 #H18 * #H19 cases(H19 I) ] 330 #s2_fin * #t2_fin **** #pre_t2_fin #EQcost #R_st3_s2_fin #Hm #Hs %{s2_fin} %{(t2_init @ t2_fin)} 331 cut(? : Prop) 332 [3: #Hpre % 333 [ % 334 [ % 335 [ %{Hpre} >get_cost_label_invariant_for_append_silent_trace_l // assumption 336  assumption 337 ] 338  #meas_suff cases(Hm ?) 339 [ #s_pre' * #t_pre' * #s_post' * #t_post' * #sil_tpost' * #l_em * #ex_em ** #EQ 340 destruct #Hcall #lem_cost %{s_pre'} %{(t2_init @ t_pre')} %{s_post'} %{t_post'} 341 %{sil_tpost'} %{l_em} %{ex_em} /4 by conj/ 342  cases meas_suff meas_suff #s_em * #t_pre inversion t_pre in ⊢ ?; 343 [ #st #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em * #ex_em 344 ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #_ * 345  #st1' #st2' #st3' #lbl #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost 346 * #l_em * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hcall #cost_lem 347 %{st3'} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/ 348 ] 349 ] 350 ] 351  * [2: * #H cases(H I)] #H inversion H [ #H9 #H10 #H11 #H12 #H13 #H14 destruct] 352 #x1 #x2 #x3 #prf3 #tl'' #Hclass' #pre_siltl'' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 353 /4 by append_silent,or_introl/ 354 ] 355  356 ] 357 @append_premeasurable_silent // 358  #lbl #EQ destruct #pre_tl #IH #s2 #Hs2 #REL 359 cases(simulate_label … sim … prf … REL) 360 [2,3: /2/] 361 #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2'''' 362 #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''') /2 by pre_silent_io/ 363 #s3 * #t_s3 **** #pre_s3 #EQcost #RElst3s3 #Hm #Hs %{s3} 364 %{(t_s2'' @ (t_ind … exe_s2''' …))} [ @(t_s2'''' @ t_s3) ] % 365 [2: * [ #H inversion H 366 [ #H22 #H23 #H24 #H25 #H26 #H27 destruct 367  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct 368 ] 369  * #H cases(H I) 370 ] 371 ] 372 % 373 [ % [2: assumption] % 374 [ @append_premeasurable_silent // %2 /2 by ex_intro/ 375 [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2'' 376 [ #H31 #H32 #H33 #H34 #H35 destruct assumption ] 377 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct 378 cases H47 #ABS @⊥ @ABS % ] 379 @append_premeasurable_silent // % // 380  whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l 381 [2: assumption] whd in ⊢ (???%); 382 >get_cost_label_invariant_for_append_silent_trace_l // 383 ] % assumption 384  #Hsuff cases(measurable_suffix_tind … Hsuff) 385 [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)} 386 % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct 387  #H @measurable_suffix_append change with ((t_ind ?????? t_s2'''')@t_s3) in ⊢ (????%); 388 @measurable_suffix_append /2/ 389 ] 390 ] 391 ] 392  #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ) 393 #pre_meas_tl #IH #s1 #class_s2 #RELst1s2 394 cases(simulate_ret_l … sim … exe_s2_s2' … RELst1s2) [2,3: /2/ ] 395 #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2''' 396 #sil_t1 #sil_t2 cases(IH … rel_s2_s2''') 397 [2: @(pre_silent_io … sil_t2) assumption] 398 #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL #Hm #Hs 399 %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % 400 [2: * [ #H inversion H 401 [ #H22 #H23 #H24 #H25 #H26 #H27 destruct 402  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct 403 ] 404  * #H cases(H I) 405 ] 406 ] 407 % 408 [ % [2: assumption] 409 % [2: whd in ⊢ (??%?); 410 >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) 411 whd in ⊢ (???%); 412 >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2)) 413 @eq_f assumption ] 414 @append_premeasurable_silent [2: //] %3 415 [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ] 416 cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1 417 [ #H49 #H50 #H51 #H52 #H53 destruct //] 418 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65 419 #ABS @⊥ @ABS % 420  #Hsuff cases(measurable_suffix_tind … Hsuff) 421 [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)} 422 % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct 423  #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%); 424 @measurable_suffix_append /2/ 425 ] 426 ] 427  #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct 428 #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2' 429 cases(simulate_call_pl … sim … post … exe_s1_s2 … REL_s1_s2') 430 [2,3: /2 by head_of_premeasurable_is_not_io/ ] 431 #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2 432 cases(IH … REL) 433 [2: /2 by pre_silent_io/ ] 434 #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL1 #Hm #Hs %{s2_fin} 435 %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % 436 [2: * [ #H inversion H 437 [ #H22 #H23 #H24 #H25 #H26 #H27 destruct 438  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct 439 ] 440  * #H cases(H I) 441 ] 442 ] 443 % 444 [ % [2: assumption] % 445 [2: whd in ⊢ (??%?); 446 >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) 447 whd in ⊢ (???%); 448 >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2)) 449 @eq_f assumption ] 450 @append_premeasurable_silent try assumption 451 %4 try assumption 452 [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //] 453 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83 454 #ABS @⊥ @ABS % 455  whd %{f} %{lab} % 456  @append_premeasurable_silent // % assumption 457 ] 458  #Hsuff cases(measurable_suffix_tind … Hsuff) 459 [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)} 460 % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % // 461  #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%); 462 @measurable_suffix_append /2/ 463 ] 464 ] 465  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 * 466 #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct 467 #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … sim … exe_12 … Hst1 … REL) [2,3: /2/ ] 468 #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1 469 #sil_tr2 #call_rel cases(IH1 … REL1) 470 [2: /2 by pre_silent_io/ ] 471 #st3' * #tr3 **** #pre_tr3 #EQcost_tr3 #REL2 #Hm1 #Hs1 472 cases(simulate_ret_n … sim … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ] 473 #st3'' * #st4' * #st4'' * 474 #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ] 475 #st5' * #tr6 **** #pre_tr6 #EQcost_tr6 #REL4 #Hm2 #Hs2 %{st5'} 476 %{(tr1 @ (t_ind … exe_12' … ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))} 477 % 478 [2: * [ #H inversion H 479 [ #H22 #H23 #H24 #H25 #H26 #H27 destruct 480  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct 481 ] 482  * #H cases(H I) 483 ] 484 ] 485 % 486 [ % [2: assumption] % 487 [ @append_premeasurable_silent try assumption %5 488 [1,2: /2 by pre_silent_io/ 489 cases sil_tr1 /2 by pre_silent_io/ inversion tr1 490 [ #H85 #H86 #H87 #H88 #H89 destruct // ] 491 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct 492 cases H107 #ABS @⊥ @ABS % 493  whd %{f} %{l} % 494  assumption 495  @append_premeasurable_silent try assumption [2: % //] 496 @append_silent_premeasurable // % // 497  @append_premeasurable_silent try assumption 498  @(RET_REL … call_rel) assumption 499  % 500 ] 501  >get_cost_label_invariant_for_append_silent_trace_l [2: // ] 502 whd in ⊢ (??%%); @eq_f >append_associative 503 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 504 [2: % // ] >append_associative 505 >get_cost_label_append in ⊢ (???%); 506 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 507 [2: % //] normalize 508 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 509 [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2 510 assumption 511 ] 512 % // 513  #Hsuff cases(measurable_suffix_tind … Hsuff) 514 [ * #_ #ABS @⊥ cases Hsuff #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em 515 * #ex_em ** inversion t_pre in ⊢ ?; 516 [2: #z1 #z2 #z3 #lb #exec #tail #_ #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) EQ 517 #EQ destruct >e0 in ABS; #ABS lapply(silent_append_l2 … ABS) ABS * [2: * #H cases(H I)] IH1 IH2 518 Hsuff e0 EQ #H inversion H 519 [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 destruct] 520 #y1 #y2 #y3 #exec #tail1 #Hclass1 #sil_tail #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct #_ * 521 ] 522 #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 523 #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] * 524  #Hsuff @measurable_suffix_append change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append 525 change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append @Hm2 526 cases(measurable_suffix_append_case … Hsuff) 527 [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?; 528 [ #H137 #H138 #H139 #H140 #H141 #H142 @⊥ 529 H142 lapply H141 H141 lapply H138 H138 lapply H140 H140 <H139 #EQ lapply t2 t2 >EQ EQ 530 #st2 #_ #EQ destruct(EQ) 531  #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 @⊥ Hsuff destruct 532 ] 533  Hsuff * #s_em * #t_pre inversion t_pre in ⊢ ?; 534 [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em ** #EQ normalize in EQ; 535 lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #_ * 536  #a1 #a2#a3 #lbl #exe #tl1 #_ #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em 537 * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hcall #Hcost 538 %{a3} %{tl1} %{s1_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /5 by conj/ 539 ] 540 ] 541 ] 542 ] 543 ] 544 qed. 545 546 547 lemma get_costlabels_of_trace_empty : ∀S : abstract_status.∀s1,s2 : S.∀t : raw_trace … s1 s2. 548 get_costlabels_of_trace … t = nil ? → pre_measurable_trace … t → silent_trace … t. 549 #S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H s1 s2 inversion H 550 [ #H1 #H2 #H3 #H4 #H5 #H6 destruct 551  #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 552  #s1 #s2 #s3 #l1 #Hclass #prf1 #tl * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 553  #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #f * #c #EQ destruct #Hs1 #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 554  #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hclass1 #Hclass3 * #f * #c #EQ destruct #Hs1 555 #pre1 #pre2 #Hs1s4 whd in match is_unlabelled_ret_act; normalize nodelta #EQ destruct #_ #_ #EQ1 #EQ2 #EQ3 #EQ4 556 destruct 557 ] 558 whd in EQ : (??%?); destruct cases lbl in prf1 EQ; lbl normalize [2: #lbl #H #EQ destruct] 559 #prf #H % %2 // cases(IH …) // cases tl in pre_meas_tl; 560 [2: #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 cases(absurd ?? H87) %] 561 #st #H1 #_ % /2 by head_of_premeasurable_is_not_io/ 562 qed. 563 564 lemma measurable_is_measurable_suffix : ∀S : abstract_status. 565 ∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t. 566 #S #si #s1 #s3 #sn #t * #_ * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ***** 567 #EQ destruct /11 width=20 by conj,ex_intro/ 568 qed. 569 570 lemma get_costlabelled_is_costlabelled : 571 ∀S : abstract_status.∀s1,s2,s3 : S. ∀l. 572 ∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3. 573 is_costlabelled_act l → 574 get_costlabels_of_trace … (t_ind … prf t) = 1 + get_costlabels_of_trace … t. 575 #S #s1 #s2 #s3 * normalize 576 [ /2 by monotonic_pred/ 577  * normalize /2 by lt_to_le, monotonic_pred/ #_ #t * 578  * normalize /2 by lt_to_le, monotonic_pred/ #_ #t * 579 ] 580 qed. 581 582 lemma silent_suffix_cancellable : ∀S : abstract_status. 583 ∀s1,s2,s2',s3,s3',s4 : S.∀l,l'. 584 ∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3. 585 ∀t2 : raw_trace … s3 s4. 586 ∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'. 587 ∀t2' : raw_trace … s3' s4. 588 is_costlabelled_act l → is_costlabelled_act l' → 589 silent_trace … t2 → silent_trace … t2' → 590 t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') → 591 s2 = s2' ∧ l = l' ∧ t1 ≃ t1'. 592 #S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2' 593 lapply prf prf lapply prf' prf' lapply t1' t1' elim t1 594 [ normalize #st * normalize 595 [ #st' #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct /3/ 596  #st1 #st2 #st3 #lbl #prf1 #tl #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 597 @⊥ lapply(silent_append_l2 … sil_t2) * [2: * #H cases(H I)] #H inversion H 598 [ #H1 #H2 #H3 #H4 #H5 #H6 destruct 599  #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl' 600 ] 601 ] 602 ] 603 #st1 #st2 #st3 #lbl #prf1 #tl #IH #t1' inversion t1' in ⊢ ?; 604 [ #st #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 605 @⊥ lapply(silent_append_l2 … sil_t2') * [2: * #H cases(H I)] #H inversion H 606 [ #H1 #H2 #H3 #H4 #H5 #H6 destruct 607  #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl 608 ] 609  #st1' #st2' #st3' #lbl' #prf1' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize 610 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct EQ cases(IH … e0) * #EQ1 #EQ2 #EQ3 destruct /3/ 611 ] 612 qed. 613 614 615 lemma prefix_of_measurable_suffix_is_premeasurable : ∀S : abstract_status. 616 ∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3. 617 ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s3 s4.∀t : raw_trace … s1 s4. 618 pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act l → 619 silent_trace … t2 → (is_call_act l → bool_to_Prop(is_call_post_label … s2)) → 620 pre_measurable_trace … t1. 621 #S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 t1 lapply t2 t2 lapply prf prf lapply s2 s2 622 lapply s3 s3 elim H t s1 s4 623 [ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?; 624 [ #H1 #H2 #H3 #H4 destruct #H5 #H6 #H7 normalize in H5; lapply(eq_to_jmeq ??? H5) H5 #H5 destruct 625  #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct 626 normalize in H19; lapply(eq_to_jmeq ??? H19) H19 #H19 destruct 627 ] 628  #st1 #st2 #st3 #lbl #prf #tl #Hclass ** 629 [ #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?; 630 [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 631 destruct * 632  #s3 #s4 #s5 #lab #exe #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); 633 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/ 634 ] 635  #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?; 636 [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 637 destruct #_ #_ #_ % // 638  #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ 639 lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/ 640 ] 641 ] 642  #st1 #st2 #st3 #lbl #Hclass #prf #tl * #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1 643 #t1 #t2 inversion t2 in ⊢ ?; 644 [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 645 destruct #_ #_ #_ % // 646  #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ 647 lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hl #sil_t1 #H1 %3 /2/ @(IH … (refl …)) /2/ 648 ] 649  #st1 #st2 #st3 #lbl #prf #tl #Hclass * #f * #c #EQ destruct #call_post #pre_tl #IH #s1 #s2 #prf1 650 #t1 #t2 inversion t2 in ⊢ ?; 651 [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 652 destruct #_ #_ #_ % // 653  #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ 654 lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hl #sil_t1 #H1 %4 /3/ @(IH … (refl …)) /2/ 655 ] 656  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hst1 #Hst3 * #f * #c #EQ destruct 657 #Hcall #pre_t1 #pre_t2 #succ whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #s1 #s2 #prf3 658 #t3 #t4 inversion t4 in ⊢ ?; 659 [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 660 destruct #_ #_ #_ % // 661  #s3 #s4 #s5 #lbl #prf4 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ 662 lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct #Hl #sil_t3 #H1 663 cut(measurable_suffix … (t1@(t_ind … prf2 t2))) 664 [ whd %{s5} %{tail} %{s1} %{t3} %{sil_t3} %{l} %{prf3} /4 by jmeq_to_eq, conj/] 665 #Hmeas cases(measurable_suffix_append_case … Hmeas) 666 [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?; 667 [ #H4 #H5 #H6 #H7 #H8 #H9 destruct 668  #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct 669 ] 670  Hmeas #Hmeas cases(measurable_suffix_tind … Hmeas) 671 [ **] Hmeas IH1 EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost 672 * #l_em * #ex_em ** #EQ destruct #H1 #H2 673 change with (t_ind … (t_base …) @ ?) in match (t_ind ???????) in e0; 674 <append_associative in e0; <append_associative #e0 675 cases(silent_suffix_cancellable … e0) // e0 * #EQ1 #EQ2 #EQ3 destruct 676 >append_associative %5 /2/ [ %{f} %{c} //] normalize 677 @(IH2 … (refl …)) /2/ 678 ] 679 ] 680 ] 681 qed. 682 683 684 lemma measurable_suffix_is_measurable: 685 ∀S : abstract_status. 686 ∀s1,s4 : S. 687 ∀t : raw_trace … s1 s4. 688 pre_measurable_trace … t → 689 2 ≤ get_costlabels_of_trace … t  → 690 measurable_suffix … t → ∃s1,s3. 691 measurable … s1 … s3 … t. 692 #S #s1 #s4 #t #pre_meas_t #Hlab * #s_em * #t_pre * #s_init * #t_post * #sil_tpost 693 * #l_em * #ex_em ** #EQ destruct #Hcall #Hcost_lem 694 >get_cost_label_append in Hlab; >append_length >get_costlabelled_is_costlabelled // 695 >(get_cost_label_silent_is_empty … sil_tpost) #CARD 696 cases(measurable_prefix_of_premeasurable … t_pre) 697 [3: cases(get_costlabels_of_trace ????) in CARD; [ /3/  #c #xc #_ % #EQ destruct] 698 2: @(prefix_of_measurable_suffix_is_premeasurable … pre_meas_t) [5: %*:] assumption 699  #s_prefix * #s_post_pre * #t_prefix * #lab * #exe1 * #t34 ** #sil_tprefix #EQ destruct #cost_lab 700 /20 width=20 by conj,ex_intro/ 701 ] 702 qed. 703 704 705 706 theorem simulates_measurable: 19 707 ∀S1,S2: abstract_status. 20 708 … … 36 724 37 725 ∃s1',s2'. measurable … s1' s2' … t'. 726 #S1 #S2 #rel #sim_rel #si #sn #t #s1 #s2 #Hmeas #s1' #Hclass #Rsi_si' 727 cases(simulates_pre_mesurable … rel … t … Rsi_si') // 728 [2: cases Hmeas //] #sn' * #t2 **** #pre_meas_t2 #EQcost #R_sn_sn' 729 #Hmeas1 #_ %{sn'} %{t2} % [% //] @(measurable_suffix_is_measurable … t2) /4 by measurable_is_measurable_suffix/ 730 <EQcost cases Hmeas #_ * #s1 * #s2 * #t_pre * #t_mid * #t_last * #l1 * #l2 * #prf1 * #prf2 ***** #EQ destruct 731 #H1 #H2 #_ #_ #_ >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // 732 >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // /2 by le_plus_a/ 733 qed. 734 735 736 38 737 39 738 theorem cerco:
Note: See TracChangeset
for help on using the changeset viewer.