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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Dynamic Semantics Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%theorem
dynsem!step_preserves_wf_thm :
          forall* {S1:st} {E1:exp} {S2:st} {E2:exp}
          forall {DSWf1: st_wf S1}
                 {DStep: step S1 E1 S2 E2}
          exists {DSWf2: st_wf S2}
          true.
%prove 2 DStep (dynsem!step_preserves_wf_thm _ DStep _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%theorem
dynsem!step*_preserves_wf_thm :
          forall* {S1:st} {E1:exp} {S2:st} {E2:exp}
          forall {DSWf1: st_wf S1}
                 {DSteps: step* S1 E1 S2 E2}
          exists {DSWf2: st_wf S2}
          true.
%prove 2 DSteps (dynsem!step*_preserves_wf_thm _ DSteps _).