Changeset 3584
- Timestamp:
- Jul 18, 2015, 4:14:51 PM (6 years ago)
- Location:
- LTS
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3582 r3584 30 30 ; return_type : DeqSet 31 31 }. 32 33 32 34 33 inductive Instructions (p : instr_params) -
LTS/variable_stack_pass.ma
r3583 r3584 439 439 qed. 440 440 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 → 441 lemma 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 → 443 442 var_to_shift_ok (\fst new_st). 444 443 ** [|#x #xs] #fp #v #val #new_st * [| #H1 #H2] whd in ⊢ (??%% → ?); [ #EQ destruct] … … 447 446 @(transitive_le … H1) >(len_update … x … EQnew_frm) // 448 447 qed. 448 (* 449 #st inversion st #l #p #IHst #v #val inversion l [#IHl #new_st inversion new_st #l' #p' 450 inversion 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 452 whd in match (frame_assign_var ???); 453 #H2 whd in match(var_to_shift_ok ?); % /3 by _/ 454 *) 449 455 450 456 lemma var_instr_bond_frame_assign_var_ok : ∀st,i,ct,v,val,new_st.
Note: See TracChangeset
for help on using the changeset viewer.