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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Machines
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;              : st -> exp -> mach.               %infix right 20 ;.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Machine Ok
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
mach_ok        : st -> exp -> type.
%name mach_ok DMachOk.
%mode mach_ok +S +E.
mach_ok_irred  : exp_irred E
		  -> mach_ok S E.
mach_ok_step   : step S E S' E'
		  -> mach_ok S E.
%terminates {} (mach_ok _ _).
%worlds () (mach_ok _ _).
%covers mach_ok +S +E.