Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/a8f11ab758754c56b2fd9ccd23cb6c41]
nat : type.
z : nat.
s : nat -> nat.
max : nat -> nat -> nat -> type.
mzz : max z z z.
mzs : {N:nat} max z (s N) (s N).
msz : {N:nat} max (s N) z (s N).
mss : {N1:nat} {N2:nat} {N:nat} max N1 N2 N -> max (s N1) (s N2) (s N).
%mode +{N1:nat} +{N2:nat} -{N3:nat} (max N1 N2 N3).
%worlds () (max _ _ _).
%total T (max T _ _).
exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.
height : exp -> nat -> type.
height/lam :
   {E:exp -> exp} {N:nat}
      ({x:exp} height x (s z) -> height (E x) N)
         -> height (lam ([x:exp] E x)) (s N).
height/app :
   {N1:nat} {N2:nat} {N:nat} {E2:exp} {E1:exp}
      max N1 N2 N -> height E2 N2 -> height E1 N1 -> height (app E1 E2) (s N).
%block var-height : block {x:exp} {_:height x (s z)}.
%mode +{E:exp} -{N:nat} (height E N).
%worlds (var-height) (height _ _).
[Closing file /home/www/twelfwiki/code/a8f11ab758754c56b2fd9ccd23cb6c41]
%% OK %%