Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/b4a767f0b505ce91b3c07367689afd52]
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 _ _).
nat-less-plus-uninhabited :
   {N1:nat} {N2:nat} {N3:nat}
      nat-less N1 N2 -> nat-plus N2 N3 N1 -> uninhabited -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:nat-less N1 N2} +{D2:nat-plus N2 N3 N1}
   -{D3:uninhabited} (nat-less-plus-uninhabited D1 D2 D3).
- :
   {X1:nat} {X2:nat} {X3:nat} {NL:nat-less X1 X2} {NP:nat-plus X2 X3 X1}
      {DU:uninhabited}
      nat-less-plus-uninhabited NL NP DU
         -> nat-less-plus-uninhabited (nat-less/s NL) (nat-plus/s NP) DU.
%worlds () (nat-less-plus-uninhabited _ _ _).
%total D1 (nat-less-plus-uninhabited D1 _ _).
uninhabited-nat-less : {N1:nat} {N2:nat} uninhabited -> nat-less N1 N2 -> type.
%mode +{D1:nat} +{D2:nat} +{D3:uninhabited} -{D4:nat-less D1 D2}
   (uninhabited-nat-less D1 D2 D3 D4).
%worlds () (uninhabited-nat-less _ _ _ _).
%total {} (uninhabited-nat-less _ _ _ _).
[Closing file /home/www/twelfwiki/code/b4a767f0b505ce91b3c07367689afd52]
%% OK %%