Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/b7e325bef0b84d2d0280f79dd4f4a4dc]
nat : type.
z : nat.
s : nat -> nat.
add : nat -> nat -> nat -> type.
%mode +{M:nat} +{N:nat} -{P:nat} (add M N P).
add/z : {N:nat} add z N N.
add/s : {M:nat} {N:nat} {P:nat} add M N P -> add (s M) N (s P).
%worlds () (add _ _ _).
%total M (add M _ _).
exp : type.
num : nat -> exp.
plus : exp -> exp -> exp.
ans : type.
anum : nat -> ans.
eval : exp -> ans -> type.
%mode +{E1:exp} -{E2:ans} (eval E1 E2).
eval/num : {N:nat} eval (num N) (anum N).
eval/plus :
   {N1:nat} {N2:nat} {N:nat} {E2:exp} {E1:exp}
      add N1 N2 N -> eval E2 (anum N2) -> eval E1 (anum N1)
         -> eval (plus E1 E2) (anum N).
%worlds () (eval _ _).
%total E (eval E _).
two : nat = s (s z).
%solve 
add two two N.
 OK
_ : add two two (s (s two)) = add/s (add/s add/z).
two_exp : exp = num two.
%solve 
eval (plus two_exp two_exp) E.
 OK
_ : eval (plus two_exp two_exp) (anum (s (s two)))
   = eval/plus (add/s (add/s add/z)) eval/num eval/num.
[Closing file /home/www/twelf/hcode/b7e325bef0b84d2d0280f79dd4f4a4dc]
%% OK %%