Changeset 2893


Ignore:
Timestamp:
Mar 16, 2013, 9:08:17 PM (4 years ago)
Author:
campbell
Message:

Add tlr_unrepeating.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2892 r2893  
    241241  @(well_cost_labelled_state_step … STEP WCLge WCLs)
    242242] qed.
     243
     244lemma soundly_labelled_exec_steps : ∀n,g,s,trace,s'.
     245  soundly_labelled_ge g →
     246  exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 →
     247  soundly_labelled_state s →
     248  soundly_labelled_state s'.
     249#n #g elim n
     250[ #s #trace #s' #_ #E whd in E:(??%%); destruct //
     251| #m #IH #s #trace #s' #SLge #EX
     252  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
     253  #SLs @(IH … SLge … EX')
     254  @(soundly_labelled_state_step … SLge STEP SLs)
     255] qed.
     256
    243257 
    244258
     
    256270  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
    257271  state_at RTLabs_ext_pcsys p m = return sm ∧
     272  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
    258273  le (max_stack_of_tlr ??? tlr (lift_some … stack_cost) fn midstack) max ∧
    259274  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
     
    282297| * #s2' #rem #_ #tlr #STACK #_
    283298%{s1'} %{s2'} % [2: %{tlr}
    284 % [ %
     299% [ % [ %
    285300  [ whd in ⊢ (??%?);
    286301    change with (make_ext_initial_state p) in match (make_initial_state ????);
    287302    >INIT' whd in ⊢ (??%?);
    288303    >EXEC1' %
    289   |
     304  | @tlr_sound_unrepeating
     305    [ @SLge
     306    | @(soundly_labelled_exec_steps … EXEC1)
     307      [ @SLge
     308      | @(proj2 … (well_cost_labelled_initial … INIT WCLP))
     309      ]
     310    ]
     311 ]|
    290312 ]|
    291313  ]
Note: See TracChangeset for help on using the changeset viewer.