Changeset 3589

Timestamp:

Jul 20, 2015, 3:48:33 PM (6 years ago)

Author:

piccolo

Message:

closed second daemon

File:

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

LTS/variable_stack_pass.ma

@@ -458 +458 @@
 frame_assign_var st v val = return new_st → 
 var_instr_bond_ok (\fst new_st) i ct.
-** [(*empty list activation frame*)|(*non empty list activation frame*)#x #xs]
-#fp #i #ct #v #val #new_st whd in ⊢(%→?→?);
-inversion(divide_continuation_on_frames ct [i]) 
-[1,3:(* divide_continuation_on_frames ct [i] is nil*)
-#IH normalize nodelta whd in ⊢(?→%→%); [#_|#ABS cases ABS]
->IH whd in match (frame_assign_var ???); inversion(new_st)
-#l #p #Hns elim l [normalize #_ %|#he #tl cases tl [|#he0 #tl0] #IHl #HN
-whd normalize in HN; destruct]
-|(*divide_continuation_on_frames not nil *)2,4:
-#lfi #llfi #IH0 #INV0 normalize nodelta] [#ABS cases ABS
-|whd in match(frame_assign_var ???); inversion(new_st) #newl #newp
-#_ normalize nodelta * #H1A #H1B
-
-inversion(assign_frame x (to_shift+v) (\fst fp) val)
-[2: #ll] #INVaf normalize nodelta
-#Hrr elim newl whd >INV0 normalize nodelta
-  [2: #ln #lln #IHl] whd >INV0 normalize nodelta try(%)
-  
-]
-
-cases daemon
-qed.
+* #act_frm #fp #i #ct #v #val * #new_st #new_fp whd in ⊢ (% → ?);
+<(append_nil … [?]) >divide_continuation_on_frame_app
+inversion(divide_continuation_on_frames …) normalize nodelta
+[|#x #xs #_] #EQdivide cases act_frm -act_frm [2,4: #y #ys] **
+#H1 #H2 #H3 change with (m_bind ?????) in ⊢ (??%? → ?);
+#H cases(bind_inversion ????? H) -H #new_frm * whd in match assign_frame;
+normalize nodelta #EQnew_frm whd in ⊢ (??%% → ?); #EQ destruct
+whd <(append_nil … [?]) >divide_continuation_on_frame_app 
+>EQdivide normalize nodelta % // % // <(len_update … y … EQnew_frm) //
+qed.
+
 
 lemma var_instr_bond_seq_ok : ∀st.