Changeset 2726


Ignore:
Timestamp:
Feb 25, 2013, 12:11:39 PM (6 years ago)
Author:
campbell
Message:

Show max stack preserved in FEMeasurable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2725 r2726  
    580580] qed.
    581581
    582 (* TODO: explicitly mention observables *)
     582
    583583theorem measured_subtrace_preserved :
    584584  ∀MS:meas_sim.
     
    608608#n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS'
    609609
     610cut (intensional_trace_of_trace C [ ] (prefix@interesting) =
     611     intensional_trace_of_trace C' [ ] (prefix'@interesting'))
     612[ >int_trace_append' >int_trace_append'
     613  <OBS0 @breakup_pair @breakup_pair @breakup_pair @breakup_pair
     614  <OBS' %
     615] #Eobs
     616
    610617%{m'} %{n'} %
    611618[ %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'}
     
    619626     ]
    620627  ]| @RETURNS'
    621   ]| cases daemon (* TODO! *)
     628  ]| <Eobs @MAX
    622629  ]
    623630| >INIT >INIT'
Note: See TracChangeset for help on using the changeset viewer.