Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/145a6adb76eaba29ac6571c6e59bd5e3]
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 _ _).
[Closing file /home/www/twelfwiki/code/145a6adb76eaba29ac6571c6e59bd5e3]
%% OK %%