Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/d1b92bd801504eb7a5c972b1d5eb23c0]
uninhabited : type.
%freeze uninhabited.
nat : type.
nat/z : nat.
nat/s : nat -> nat.
nat-less : nat -> nat -> type.
nat-less/z : {N:nat} nat-less nat/z (nat/s N).
nat-less/s : {N1:nat} {N2:nat} nat-less N1 N2 -> nat-less (nat/s N1) (nat/s N2).
nat-plus : nat -> nat -> nat -> type.
nat-plus/z : {N:nat} nat-plus nat/z N N.
nat-plus/s :
   {N1:nat} {N2:nat} {N3:nat}
      nat-plus N1 N2 N3 -> nat-plus (nat/s N1) N2 (nat/s N3).
nat-less-z-uninhabited : {N:nat} nat-less N nat/z -> uninhabited -> type.
%mode +{N:nat} +{D1:nat-less N nat/z} -{D2:uninhabited} (nat-less-z-uninhabited D1 D2).
%worlds () (nat-less-z-uninhabited _ _).
%total {} (nat-less-z-uninhabited _ _).
[Closing file /home/www/twelfwiki/code/d1b92bd801504eb7a5c972b1d5eb23c0]
%% OK %%