Ignore:
Timestamp:
Feb 19, 2013, 7:24:20 PM (7 years ago)
Author:
campbell
Message:

Don't apply inv in after_n_steps to last state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2677 r2682  
    10211021    >shift_fst whd in match (seq_of_labeled_statement ?);
    10221022    cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
    1023     #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/
     1023    #n #H %{(S n)} @(after_n_m 1 (S n) … H) // % /2/
    10241024    #trx #sx * /3/
    10251025(* but for LScase it's just like the cases in step_with_labels_partial *)
Note: See TracChangeset for help on using the changeset viewer.