Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/0dfa71ced85e1fabe50b0a8b8a7ffd92]
nat : type.
s : nat -> nat.
z : nat.
plus : nat -> nat -> nat -> type.
p-z : {N:nat} plus z N N.
p-s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
plus-z-thm : {N:nat} plus N z N -> type.
- : plus-z-thm z p-z.
- : {N:nat} {D:plus N z N} plus-z-thm N D -> plus-z-thm (s N) (p-s D).
%mode +{N:nat} -{D:plus N z N} (plus-z-thm N D).
%worlds () (plus-z-thm _ _).
%total T (plus-z-thm T _).
[Closing file /home/www/twelf/hcode/0dfa71ced85e1fabe50b0a8b8a7ffd92]
%% OK %%