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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Loc Less-than Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

loc!lt_trans   : loc_lt L1 L2 -> loc_lt L2 L3 -> loc_lt L1 L3 -> type.
%mode loc!lt_trans +DLocLt12 +DLocLt23 -DLocLt13.
-              : loc!lt_trans (loc_lt_ DNatLt12) 
                              (loc_lt_ DNatLt23) 
                              (loc_lt_ DNatLt13)
		  <- nat!lt_trans DNatLt12 DNatLt23 DNatLt13.
%worlds () (loc!lt_trans _ _ _).
%total DLocLt12 (loc!lt_trans DLocLt12 _ _).

loc!lt_contradict
               : loc_lt L L -> absurd -> type.
%mode loc!lt_contradict +DLocLt -Absurd.
-              : loc!lt_contradict (loc_lt_ DNatLt) Absurd
		  <- nat!lt_contradict DNatLt Absurd.
%worlds () (loc!lt_contradict _ _).
%total DLocLt (loc!lt_contradict DLocLt _).