Ignore:
Timestamp:
Feb 6, 2013, 5:03:18 PM (7 years ago)
Author:
campbell
Message:

Tidy up measurable a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2597 r2618  
    1313  ms_C2 : preclassified_system;
    1414  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
    15   ms_inv : ? → ? → Prop;
     15  ms_inv : ? → ? → Type[0];
     16  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
    1617  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
    1718  sim_normal :
     
    7374  ms_rel MS g1 g2 INV s1 s1' →
    7475  ∀m,prefix,suffix.
    75   split_trace (ms_C1 MS) ? trace m = Some ? 〈prefix,suffix〉 →
    76   le (max_stack (ms_C1 MS) prefix) max_allowed_stack →
     76  split_trace ? trace m = Some ? 〈prefix,suffix〉 →
     77  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack →
    7778  ∃m',prefix',suffix'.
    78   split_trace (ms_C2 MS) ? trace' m' = Some ? 〈prefix',suffix'〉 ∧
    79   le (max_stack (ms_C1 MS) prefix') max_allowed_stack ∧
     79  split_trace ? trace' m' = Some ? 〈prefix',suffix'〉 ∧
     80  le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
    8081  ∃s2,s2'. trace_starts ? suffix s2 ∧ trace_starts ? suffix' s2' ∧
    81     ms_rel g1 g2 INV s2 s2'.
     82    ms_rel MS g1 g2 INV s2 s2'.
    8283
    8384theorem measured_subtrace_preserved :
Note: See TracChangeset for help on using the changeset viewer.