Ignore:
Timestamp:
Mar 15, 2013, 6:33:18 PM (8 years ago)
Author:
piccolo
Message:

partial commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2879 r2883  
    146146  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    147147  repeat_eval_seq_no_pc p curr_id b st = return st' →
    148   trace_any_any_free (joint_abstract_status p) st
    149     (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
     148  Σtaaf :trace_any_any_free (joint_abstract_status p) st
     149    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     150    (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
    150151  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3.
    151152  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3.
     
    175176  #H #G
    176177  %2{(taa_base …)} assumption
    177 | #hd #tl #_ #EQ <EQ -hd -tl @produce_trace_any_any_free assumption
     178| #hd #tl #_ #EQ <EQ -hd -tl #H1 #H2 @(produce_trace_any_any_free …) assumption
    178179]
    179180qed.
Note: See TracChangeset for help on using the changeset viewer.