Changeset 3584


Ignore:
Timestamp:
Jul 18, 2015, 4:14:51 PM (4 years ago)
Author:
pellitta
Message:
 
Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3582 r3584  
    3030; return_type : DeqSet
    3131}.
    32 
    3332
    3433inductive Instructions (p : instr_params)
  • LTS/variable_stack_pass.ma

    r3583 r3584  
    439439qed.
    440440
    441 lemma var_to_shift_frame_assign_var_ok : ∀st,v,val,new_st.
    442 var_to_shift_ok (\fst st) → frame_assign_var st v val = return new_st →
     441lemma var_to_shift_frame_assign_var_ok : ∀st,v,val,new_st.var_to_shift_ok (\fst st) → frame_assign_var st v val = return new_st →
    443442var_to_shift_ok (\fst new_st).
    444443** [|#x #xs] #fp #v #val #new_st * [| #H1 #H2] whd in ⊢ (??%% → ?); [ #EQ destruct]
     
    447446@(transitive_le … H1) >(len_update … x … EQnew_frm) //
    448447qed.
     448(*
     449#st inversion st #l #p #IHst #v #val inversion l [#IHl #new_st inversion new_st #l' #p'
     450inversion l' [#IHl' #IHnew_st #H #H18 @H|#ln #lln whd in match(var_to_shift_ok ?); whd in match(var_to_shift_ok ?); whd in match(var_to_shift_ok ?); #H #IHl' destruct
     451#H2 #_ destruct
     452whd in match (frame_assign_var ???);
     453#H2 whd in match(var_to_shift_ok ?); % /3 by _/
     454*)
    449455
    450456lemma var_instr_bond_frame_assign_var_ok : ∀st,i,ct,v,val,new_st.
Note: See TracChangeset for help on using the changeset viewer.