Changeset 3509

Timestamp:

Sep 26, 2014, 6:12:07 PM (6 years ago)

Author:

sacerdot

Message:

...

File:

• LTS/Final.ma (modified) (4 diffs)

LTS/Final.ma

@@ -37 +37 @@
  ∃s1',s2'. measurable … s1' s2' … t'.
 
-axiom cerco:
+theorem cerco:
  (* Given the operational semantics of a source program *)
  ∀S1: abstract_status.
@@ -68 +68 @@
  (* There exists a corresponding target trace starting from si' *)
  ∃sn'. ∃t': raw_trace … si' sn'.
-  Srel … sn sn' ∧
-  get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧ 
+  Srel … rel sn sn' ∧
+  ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'. 
  
  (* that has a measurable fragment starting in s1' and ending in s2' *)
@@ -90 +90 @@
    obtained by applying every semantics in abs_trace. *)
  R s2' (〚abs_actions〛 a1).
-[2: @hide_prf
+[2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf
     cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
     #lbl' #pc * #Hmem #EQ destruct
@@ -96 +96 @@
     @(proj2 … (static_analisys_ok … EQmap … Hmem))
 ]
+cases daemon
+qed.