Changeset 3583

Timestamp:

Jul 16, 2015, 5:09:09 PM (4 years ago)

Author:

piccolo

Message:

closed first daemon

File:

• LTS/variable_stack_pass.ma (modified) (1 diff)

LTS/variable_stack_pass.ma

@@ -442 +442 @@
 var_to_shift_ok (\fst st) → frame_assign_var st v val = return new_st → 
 var_to_shift_ok (\fst new_st).
-cases daemon
+** [|#x #xs] #fp #v #val #new_st * [| #H1 #H2] whd in ⊢ (??%% → ?); [ #EQ destruct]
+whd in match assign_frame; normalize nodelta inversion(update  …) normalize nodelta
+[ #_ #EQ destruct] #new_frm #EQnew_frm whd in ⊢ (??%% → ?); #EQ destruct % // 
+@(transitive_le … H1) >(len_update … x … EQnew_frm) //
 qed.