Changeset 3509 for LTS/Final.ma


Ignore:
Timestamp:
Sep 26, 2014, 6:12:07 PM (5 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Final.ma

    r3507 r3509  
    3737 ∃s1',s2'. measurable … s1' s2' … t'.
    3838
    39 axiom cerco:
     39theorem cerco:
    4040 (* Given the operational semantics of a source program *)
    4141 ∀S1: abstract_status.
     
    6868 (* There exists a corresponding target trace starting from si' *)
    6969 ∃sn'. ∃t': raw_trace … si' sn'.
    70   Srel … sn sn' ∧
    71   get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧
     70  Srel … rel sn sn' ∧
     71  ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'.
    7272 
    7373 (* that has a measurable fragment starting in s1' and ending in s2' *)
     
    9090   obtained by applying every semantics in abs_trace. *)
    9191 R s2' (〚abs_actions〛 a1).
    92 [2: @hide_prf
     92[2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf
    9393    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
    9494    #lbl' #pc * #Hmem #EQ destruct
     
    9696    @(proj2 … (static_analisys_ok … EQmap … Hmem))
    9797]
     98cases daemon
     99qed.
Note: See TracChangeset for help on using the changeset viewer.