Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/7d1959a4ee8e6daf9066fd4d734b74b4]
nat : type.
z : nat.
s : nat -> nat.
sum : nat -> nat -> nat -> type.
sum/z : {N:nat} sum z N N.
sum/s : {N:nat} {M:nat} {P:nat} sum N M P -> sum (s N) M (s P).
lt : nat -> nat -> type.
lt/z : {N:nat} lt z (s N).
lt/s : {N:nat} {M:nat} lt N M -> lt (s N) (s M).
even : nat -> type.
odd : nat -> type.
sum-ident : {N:nat} sum N z N -> type.
%mode +{N:nat} -{D:sum N z N} (sum-ident N D).
- : sum-ident z sum/z.
- : {N:nat} {D:sum N z N} sum-ident N D -> sum-ident (s N) (sum/s D).
%worlds () (sum-ident _ _).
%total N (sum-ident N _).
sum-incr : {N:nat} {M:nat} {P:nat} sum N M P -> sum N (s M) (s P) -> type.
%mode +{N:nat} +{M:nat} +{P:nat} +{D1:sum N M P} -{D2:sum N (s M) (s P)}
   (sum-incr D1 D2).
- : {N:nat} sum-incr sum/z sum/z.
- :
   {N:nat} {M:nat} {P:nat} {D:sum N M P} {D':sum N (s M) (s P)}
      sum-incr D D' -> sum-incr (sum/s D) (sum/s D').
%worlds () (sum-incr _ _).
%total D (sum-incr D _).
sum-commutes : {N:nat} {M:nat} {P:nat} sum N M P -> sum M N P -> type.
%mode +{N:nat} +{M:nat} +{P:nat} +{D1:sum N M P} -{D2:sum M N P} (sum-commutes D1 D2).
- : {N:nat} {D:sum N z N} sum-ident N D -> sum-commutes sum/z D.
- :
   {M:nat} {N:nat} {P:nat} {D':sum M N P} {D'':sum M (s N) (s P)} {D:sum N M P}
      sum-incr D' D'' -> sum-commutes D D' -> sum-commutes (sum/s D) D''.
%worlds () (sum-commutes _ _).
%total D (sum-commutes D _).
[Closing file /home/www/twelf/hcode/7d1959a4ee8e6daf9066fd4d734b74b4]
%% OK %%