Changeset 3584

Timestamp:

Jul 18, 2015, 4:14:51 PM (4 years ago)

Author:

pellitta

Message:

 

Location:

LTS

Files:

• Language.ma (modified) (1 diff)
• variable_stack_pass.ma (modified) (2 diffs)

LTS/Language.ma

@@ -30 +30 @@
 ; return_type : DeqSet
 }.
-
 
 inductive Instructions (p : instr_params) 

LTS/variable_stack_pass.ma

@@ -439 +439 @@
 qed.
 
-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 → 
+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 → 
 var_to_shift_ok (\fst new_st).
 ** [|#x #xs] #fp #v #val #new_st * [| #H1 #H2] whd in ⊢ (??%% → ?); [ #EQ destruct]
@@ -447 +446 @@
 @(transitive_le … H1) >(len_update … x … EQnew_frm) //
 qed.
+(*
+#st inversion st #l #p #IHst #v #val inversion l [#IHl #new_st inversion new_st #l' #p'
+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
+#H2 #_ destruct
+whd in match (frame_assign_var ???); 
+#H2 whd in match(var_to_shift_ok ?); % /3 by _/
+*)
 
 lemma var_instr_bond_frame_assign_var_ok : ∀st,i,ct,v,val,new_st.