Changeset 3507 for LTS/Vm.ma


Ignore:
Timestamp:
Sep 26, 2014, 5:44:34 PM (5 years ago)
Author:
sacerdot
Message:

New file to contain the final statements of CerCo?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3506 r3507  
    11621162  dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
    11631163
    1164 (* Given an abstract state in relation with the second state of the trace *)
     1164(* Given an abstract state in relation with the first state of the measurable
     1165   fragment *)
    11651166∀a1.R s1 a1 →
    11661167
    1167 (* The final state of the trace is in relation with the one obtained by
    1168    applying every semantics in abs_trace. *)
     1168(* The final state of the measurable fragment is in relation with the one
     1169   obtained by applying every semantics in abs_trace. *)
    11691170R s2 (〚abs_actions〛 a1).
    11701171[2: @hide_prf
Note: See TracChangeset for help on using the changeset viewer.