 Timestamp:
 Mar 16, 2013, 9:08:16 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2839 r2892 218 218 >STEPS'' % 219 219 ] qed. 220 220 221 lemma label_to_return_state_labelled : ∀C,n,s,trace,s'. 222 trace_is_label_to_return C trace → 223 exec_steps n ?? C ? s = OK ? 〈trace,s'〉 → 224 cs_labelled C s. 225 #C #n #s #trace #s' 226 * #tr * #s1 * #trace' * #tr' * #s2 * * #E #CS #_ destruct 227 #EX >(exec_steps_first … EX) 228 @CS 229 qed. 230 231 lemma well_cost_labelled_exec_steps : ∀n,g,s,trace,s'. 232 well_cost_labelled_ge g → 233 exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 → 234 well_cost_labelled_state s → 235 well_cost_labelled_state s'. 236 #n #g elim n 237 [ #s #trace #s' #_ #E whd in E:(??%%); destruct // 238  #m #IH #s #trace #s' #WCLge #EX 239 cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX' 240 #WCLs @(IH … WCLge … EX') 241 @(well_cost_labelled_state_step … STEP WCLge WCLs) 242 ] qed. 221 243 222 244 … … 228 250 229 251 theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting. 252 well_cost_labelled_program p → 230 253 measurable RTLabs_pcsys p m n stack_cost max → 231 254 observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 → … … 236 259 pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting. 237 260 #p #m #n #stack_cost #max #prefix #interesting 261 #WCLP cases (well_cost_labelled_make_global p WCLP) 238 262 change with (make_global … RTLabs_fullexec p) in match (make_global p); 263 #WCLge #SLge 239 264 * #s0 * #prefix' * #s1 * #interesting' * #s2 240 265 letin ge ≝ (make_global … RTLabs_fullexec p) … … 249 274 lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????) 250 275 [ @will_return_equiv assumption 251  252  253  276  @(label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) 277  @(well_cost_labelled_exec_steps … EXEC1) 278 [ assumption 279  @(proj1 … (well_cost_labelled_initial … INIT WCLP)) 280 ] 281  @WCLge 254 282  * #s2' #rem #_ #tlr #STACK #_ 255 283 %{s1'} %{s2'} % [2: %{tlr}
Note: See TracChangeset
for help on using the changeset viewer.