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

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

dynsem!step_preserves_wf        
               : st_wf S1 -> step S1 E1 S2 E2 -> st_wf S2 -> type.
%mode dynsem!step_preserves_wf +DSWf1 +DStep -DSWf2.
-lam_alloc     : dynsem!step_preserves_wf DSWf (lam_alloc_step DStAlloc) DSWf'
		  <- st!alloc_preserves_wf DSWf DStAlloc DSWf'.
-app_ctxt1     : dynsem!step_preserves_wf DSWf (app_ctxt1_step DStep) DSWf'
		  <- dynsem!step_preserves_wf DSWf DStep DSWf'.
-app_ctxt2     : dynsem!step_preserves_wf DSWf (app_ctxt2_step DStep) DSWf'
		  <- dynsem!step_preserves_wf DSWf DStep DSWf'.
-app_beta      : dynsem!step_preserves_wf DSWf (app_beta_step _) DSWf.
-unit_alloc    : dynsem!step_preserves_wf DSWf (unit_alloc_step DStAlloc) DSWf'
		  <- st!alloc_preserves_wf DSWf DStAlloc DSWf'.
-letunit_ctxt  : dynsem!step_preserves_wf DSWf (letunit_ctxt_step DStep) DSWf'
		  <- dynsem!step_preserves_wf DSWf DStep DSWf'.
-letunit_beta  : dynsem!step_preserves_wf DSWf (letunit_beta_step _) DSWf.
-pair_ctxt1    : dynsem!step_preserves_wf DSWf (pair_ctxt1_step DStep) DSWf'
		  <- dynsem!step_preserves_wf DSWf DStep DSWf'.
-pair_ctxt2    : dynsem!step_preserves_wf DSWf (pair_ctxt2_step DStep) DSWf'
		  <- dynsem!step_preserves_wf DSWf DStep DSWf'.
-pair_alloc    : dynsem!step_preserves_wf DSWf (pair_alloc_step DStAlloc) DSWf'
		  <- st!alloc_preserves_wf DSWf DStAlloc DSWf'.
-letpair_ctxt  : dynsem!step_preserves_wf DSWf (letpair_ctxt_step DStep) DSWf'
		  <- dynsem!step_preserves_wf DSWf DStep DSWf'.
-letpair_beta  : dynsem!step_preserves_wf DSWf (letpair_beta_step _) DSWf.
%terminates DStep (dynsem!step_preserves_wf _ DStep _).
%worlds () (dynsem!step_preserves_wf _ _ _).
%covers dynsem!step_preserves_wf +DSWf1 +DStep -DSWf2.
%total DStep (dynsem!step_preserves_wf _ DStep _).

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

dynsem!step*_preserves_wf       
               : st_wf S1 -> step* S1 E1 S2 E2 -> st_wf S2 -> type.
%mode dynsem!step*_preserves_wf +DSWf1 +DSteps -DSWf2.
-refl          : dynsem!step*_preserves_wf DSWf (refl_step*) DSWf.
-trans         : dynsem!step*_preserves_wf DSWf1 (trans_step* DSteps23 DSteps12) DSWf3
		  <- dynsem!step*_preserves_wf DSWf1 DSteps12 DSWf2
		  <- dynsem!step*_preserves_wf DSWf2 DSteps23 DSWf3.
-step          : dynsem!step*_preserves_wf DSWf (step_step* DStep) DSWf'
		  <- dynsem!step_preserves_wf DSWf DStep DSWf'.
%terminates DSteps (dynsem!step*_preserves_wf _ DSteps _).
%worlds () (dynsem!step*_preserves_wf _ _ _).
%covers dynsem!step*_preserves_wf +DSWf1 +DSteps -DSWf2.
%total DSteps (dynsem!step*_preserves_wf _ DSteps _).