Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/d24d346820a824e989b19a8b5ea45a09]
nat : type.
nat/z : nat.
nat/s : nat -> nat.
lex : nat -> type.
lex/z : lex nat/z.
lex/s : {N:nat} nat -> lex N -> lex (nat/s N).
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).
lex-less : {X1:nat} {X2:nat} lex X1 -> lex X2 -> type.
lex-less/z : {X1:nat} {X2:nat} {X3:lex X1} lex-less lex/z (lex/s X2 X3).
lex-less/eq :
   {X1:nat} {X2:nat} {NL1:lex X1} {NL2:lex X2} {N1:nat}
      lex-less NL1 NL2 -> lex-less (lex/s N1 NL1) (lex/s N1 NL2).
lex-less/gt :
   {N2:nat} {N1:nat} {X1:nat} {X2:nat} {X3:lex X1} {X4:lex X2}
      nat-less N2 N1 -> lex-less (lex/s N1 X3) (lex/s N2 X4).
nat-less-trans :
   {N1:nat} {N2:nat} {N3:nat}
      nat-less N1 N2 -> nat-less N2 N3 -> nat-less N1 N3 -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:nat-less N1 N2} +{D2:nat-less N2 N3}
   -{D3:nat-less N1 N3} (nat-less-trans D1 D2 D3).
- :
   {X1:nat} {X2:nat} {X3:nat-less (nat/s X1) (nat/s X2)}
      nat-less-trans nat-less/z X3 nat-less/z.
- :
   {X1:nat} {X2:nat} {X3:nat} {N1:nat-less X1 X2} {N2:nat-less X2 X3}
      {N3:nat-less X1 X3}
      nat-less-trans N1 N2 N3
         -> nat-less-trans (nat-less/s N1) (nat-less/s N2) (nat-less/s N3).
%worlds () (nat-less-trans _ _ _).
%total {D1} (nat-less-trans D1 _ _).
nat-less-immsucc : {N:nat} nat-less N (nat/s N) -> type.
%mode +{D1:nat} -{D2:nat-less D1 (nat/s D1)} (nat-less-immsucc D1 D2).
- : nat-less-immsucc nat/z nat-less/z.
- :
   {N1:nat} {NL:nat-less N1 (nat/s N1)}
      nat-less-immsucc N1 NL -> nat-less-immsucc (nat/s N1) (nat-less/s NL).
%worlds () (nat-less-immsucc _ _).
%total {D1} (nat-less-immsucc D1 _).
lex-less-trans :
   {X1:nat} {X2:nat} {NL1:lex X1} {NL2:lex X2} {X3:nat} {NL3:lex X3}
      lex-less NL1 NL2 -> lex-less NL2 NL3 -> lex-less NL1 NL3 -> type.
%mode +{X1:nat} +{X2:nat} +{NL1:lex X1} +{NL2:lex X2} +{X3:nat} +{NL3:lex X3}
   +{D1:lex-less NL1 NL2} +{D2:lex-less NL2 NL3} -{D3:lex-less NL1 NL3}
   (lex-less-trans D1 D2 D3).
- :
   {X1:nat} {X2:nat} {X3:lex X1} {X4:nat} {X5:nat} {X6:lex X4}
      {X7:lex-less (lex/s X2 X3) (lex/s X5 X6)}
      lex-less-trans lex-less/z X7 lex-less/z.
- :
   {X1:nat} {X2:nat} {X3:lex X1} {X4:lex X2} {X5:nat} {X6:lex X5}
      {NL1:lex-less X3 X4} {NL2:lex-less X4 X6} {NL3:lex-less X3 X6} {X7:nat}
      lex-less-trans NL1 NL2 NL3
         -> lex-less-trans (lex-less/eq NL1) (lex-less/eq NL2) (lex-less/eq NL3).
- :
   {X1:nat} {X2:nat} {X3:nat} {NL2:nat-less X1 X2} {NL1:nat-less X2 X3}
      {NL3:nat-less X1 X3} {X4:nat} {X5:nat} {X6:lex X4} {X7:lex X5} {X8:nat}
      {X9:lex X8}
      nat-less-trans NL2 NL1 NL3
         -> lex-less-trans (lex-less/gt NL1) (lex-less/gt NL2) (lex-less/gt NL3).
- :
   {X1:nat} {X2:nat} {X3:nat} {X4:lex X1} {X5:nat} {X6:lex X2} {X7:nat}
      {X8:lex X7} {NL:nat-less X5 X3} {X9:lex-less X6 X8}
      lex-less-trans (lex-less/gt NL) (lex-less/eq X9) (lex-less/gt NL).
- :
   {X1:nat} {X2:nat} {X3:nat} {X4:lex X1} {X5:lex X2} {X6:nat} {X7:nat}
      {X8:lex X6} {X9:lex-less X4 X5} {NL:nat-less X7 X3}
      lex-less-trans (lex-less/eq X9) (lex-less/gt NL) (lex-less/gt NL).
%worlds () (lex-less-trans _ _ _).
%total {D1} (lex-less-trans D1 _ _).
lex-less-succ :
   {X1:nat} {X2:nat} {LL':lex X2} {LL:lex X1} lex-less LL LL' -> type.
%mode +{X1:nat} -{X2:nat} -{LL':lex X2} +{D1:lex X1} -{D2:lex-less D1 LL'}
   (lex-less-succ D1 D2).
- : lex-less-succ lex/z lex-less/z.
- :
   {X1:nat} {X2:nat} {X3:lex X2} {NL:lex X1} {NLL:lex-less NL X3} {N:nat}
      lex-less-succ NL NLL -> lex-less-succ (lex/s N NL) (lex-less/eq NLL).
%worlds () (lex-less-succ _ _).
%total {N} (lex-less-succ N _).
lex-less-dense :
   {X1:nat} {X2:nat} {N1:lex X1} {N3:lex X2} {X3:nat} {N2:lex X3}
      lex-less N1 N3 -> lex-less N1 N2 -> lex-less N2 N3 -> type.
%mode +{X1:nat} +{X2:nat} +{N1:lex X1} +{N3:lex X2} -{X3:nat} -{N2:lex X3}
   +{D1:lex-less N1 N3} -{D2:lex-less N1 N2} -{D3:lex-less N2 N3}
   (lex-less-dense D1 D2 D3).
- :
   {N:nat} {NL:nat-less N (nat/s N)} {X1:nat} {X2:lex X1}
      nat-less-immsucc N NL
         -> lex-less-dense lex-less/z lex-less/z (lex-less/gt NL).
- :
   {X1:nat} {X2:nat} {X3:lex X1} {X4:lex X2} {X5:nat} {X6:lex X5}
      {LL:lex-less X3 X4} {LL1:lex-less X3 X6} {LL2:lex-less X6 X4} {X7:nat}
      lex-less-dense LL LL1 LL2
         -> lex-less-dense (lex-less/eq LL) (lex-less/eq LL1) (lex-less/eq LL2).
- :
   {X1:nat} {X2:nat} {X3:lex X2} {X4:lex X1} {LL:lex-less X4 X3} {X5:nat}
      {X6:nat} {X7:nat} {X8:lex X5} {NL:nat-less X7 X6}
      lex-less-succ X4 LL
         -> lex-less-dense (lex-less/gt NL) (lex-less/eq LL) (lex-less/gt NL).
%worlds () (lex-less-dense _ _ _).
%total {D1} (lex-less-dense D1 _ _).
uninhabited : type.
%freeze uninhabited.
nat-less-refl-uninhabited : {N1:nat} nat-less N1 N1 -> uninhabited -> type.
%mode +{N1:nat} +{D1:nat-less N1 N1} -{D2:uninhabited}
   (nat-less-refl-uninhabited D1 D2).
- :
   {X1:nat} {NL:nat-less X1 X1} {DU:uninhabited}
      nat-less-refl-uninhabited NL DU
         -> nat-less-refl-uninhabited (nat-less/s NL) DU.
%worlds () (nat-less-refl-uninhabited _ _).
%total {D1} (nat-less-refl-uninhabited D1 _).
lex-less-refl-uninhabited :
   {X1:nat} {LL:lex X1} lex-less LL LL -> uninhabited -> type.
%mode +{X1:nat} +{LL:lex X1} +{D1:lex-less LL LL} -{D2:uninhabited}
   (lex-less-refl-uninhabited D1 D2).
- :
   {X1:nat} {X2:lex X1} {LL:lex-less X2 X2} {DU:uninhabited} {X3:nat}
      lex-less-refl-uninhabited LL DU
         -> lex-less-refl-uninhabited (lex-less/eq LL) DU.
- :
   {X1:nat} {DL:nat-less X1 X1} {DU:uninhabited} {X2:nat} {X3:lex X2}
      nat-less-refl-uninhabited DL DU
         -> lex-less-refl-uninhabited (lex-less/gt DL) DU.
%worlds () (lex-less-refl-uninhabited _ _).
%total {DU} (lex-less-refl-uninhabited DU _).
[Closing file /home/www/twelfwiki/code/d24d346820a824e989b19a8b5ea45a09]
%% OK %%