%%% Simply Typed Lambda Calculus w/ small-step, allocation semantics
%%% Author: Matthew Fluet (June 2005)
%%% store-lemmas.elf

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store WF Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

st!wf_tail     : st_wf (cons_st L V S') -> st_wf S' -> type.
%mode st!wf_tail +DSWf -DSWf'.
-cons_nil      : st!wf_tail (st_wf_cons_nil) st_wf_nil.
-cons_cons     : st!wf_tail (st_wf_cons_cons DSWf' _) DSWf'.
%terminates {} (st!wf_tail _ _).
%worlds () (st!wf_tail _ _).
%covers st!wf_tail +DSWf -DSWf'.
%total {} (st!wf_tail _ _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Alloc Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

st!alloc_preserves_wf    
               : st_wf S1 -> st_alloc S1 V S2 L -> st_wf S2 -> type.
%mode st!alloc_preserves_wf +DSWf1 +DStAlloc -DSWf2.
-nil           : st!alloc_preserves_wf (st_wf_nil)
                                       (st_alloc_nil)
                                       (st_wf_cons_nil).
-cons          : st!alloc_preserves_wf DSWf
                                       (st_alloc_cons)
                                       (st_wf_cons_cons DSWf (loc_lt_ DNatLt))
		 <- nat!N_lt_sN _ DNatLt.
%terminates DStAlloc (st!alloc_preserves_wf _ DStAlloc _).
%worlds () (st!alloc_preserves_wf _ _ _).
%covers st!alloc_preserves_wf +DSWf1 +DStAlloc -DStWf2.
%total DStAlloc (st!alloc_preserves_wf _ DStAlloc _).