Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/3bf88d2569630a5e2dc907f83c54a318]
tp : type.
unit : tp.
arrow : tp -> tp -> tp.
tm : type.
empty : tm.
lam : tp -> (tm -> tm) -> tm.
app : tm -> tm -> tm.
nat : type.
z : nat.
s : nat -> nat.
plus : nat -> nat -> nat -> type.
%mode +{X1:nat} +{X2:nat} -{X3:nat} (plus X1 X2 X3).
plus-z : {N2:nat} plus z N2 N2.
plus-s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
%worlds () (plus _ _ _).
%total N (plus N _ _).
size : tm -> nat -> type.
%mode +{E:tm} -{N:nat} (size E N).
size-empty : size empty (s z).
size-lam :
   {E:tm -> tm} {N:nat} {X1:tp}
      ({x:tm} size x (s z) -> size (E x) N) -> size (lam X1 ([x:tm] E x)) (s N).
size-app :
   {N1:nat} {N2:nat} {N:nat} {E2:tm} {E1:tm}
      plus N1 N2 N -> size E2 N2 -> size E1 N1 -> size (app E1 E2) (s N).
[Closing file /home/www/twelf/hcode/3bf88d2569630a5e2dc907f83c54a318]
%% OK %%