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

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

%theorem
st!wf_tail_thm : 
          forall* {L:loc} {V:val} {S':st}
          forall {DSWf: st_wf (cons_st L V S')}
          exists {DSWf': st_wf S'}
          true.
%prove 2 {} (st!wf_tail_thm _ _).

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

%theorem
st!alloc_preserves_wf_thm :
          forall* {S1:st} {V:val} {S2:st} {L:loc}
          forall {DSWf1: st_wf S1}
                 {DStAlloc: st_alloc S1 V S2 L}
          exists {DSWf2: st_wf S2}
          true.
%prove 4 DStAlloc (st!alloc_preserves_wf_thm _ DStAlloc _).