Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/d4b45c2ee1ae52a4458381730b1132a9]
nat : type.
z : nat.
s : nat -> nat.
even : nat -> type.
even-z : even z.
even-s : {N:nat} even N -> even (s (s N)).
plus : nat -> nat -> nat -> type.
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).
sum-evens :
   {N1:nat} {N2:nat} {N3:nat}
      even N1 -> even N2 -> plus N1 N2 N3 -> even N3 -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:even N1} +{D2:even N2} +{D3:plus N1 N2 N3}
   -{D4:even N3} (sum-evens D1 D2 D3 D4).
sez : {N2:nat} {DevenN2:even N2} sum-evens even-z DevenN2 plus-z DevenN2.
ses :
   {N1':nat} {N2:nat} {N3':nat} {DevenN1':even N1'} {DevenN2:even N2}
      {Dplus:plus N1' N2 N3'} {DevenN3':even N3'}
      sum-evens DevenN1' DevenN2 Dplus DevenN3'
         -> sum-evens (even-s DevenN1') DevenN2 (plus-s (plus-s Dplus))
               (even-s DevenN3').
%worlds () (sum-evens _ _ _ _).
%total D (sum-evens D _ _ _).
[Closing file /home/www/twelf/hcode/d4b45c2ee1ae52a4458381730b1132a9]
%% OK %%