Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/5bbc1b024cc897579871fc26f81ba453]
t : type.
nat_sort : type = t -> t -> t.
even : t -> t -> t = [even:t] [odd:t] even.
odd : t -> t -> t = [even1:t] [odd:t] odd.
add1-mod2 : (t -> t -> t) -> t -> t -> t
   = [s:t -> t -> t] [even1:t] [odd1:t] s odd1 even1.
nat : (t -> t -> t) -> type.
z : nat ([x:t] [x1:t] x).
s : {X:t -> t -> t} nat ([x:t] [x1:t] X x x1) -> nat ([x:t] [x1:t] X x1 x).
const_even : (t -> t -> t) -> t -> t -> t
   = [s1:t -> t -> t] [even1:t] [odd1:t] s1 even1 even1.
const_odd : (t -> t -> t) -> t -> t -> t
   = [s1:t -> t -> t] [even1:t] [odd1:t] s1 odd1 odd1.
identity : (t -> t -> t) -> t -> t -> t
   = [s1:t -> t -> t] [even1:t] [odd1:t] s1 even1 odd1.
plus_min :
   {X:t -> t -> t} {Y:t -> t -> t} {Z:t -> t -> t}
      nat ([x:t] [x1:t] X x x1) -> nat ([x:t] [x1:t] Y x x1)
         -> nat ([x:t] [x1:t] Z x x1) -> type.
%mode +{X:t -> t -> t} +{Y:t -> t -> t} -{Z:t -> t -> t}
   +{N1:nat ([x:t] [x1:t] X x x1)} +{N2:nat ([x:t] [x1:t] Y x x1)}
   -{N3:nat ([x:t] [x1:t] Z x x1)} (plus_min N1 N2 N3).
plus_min_z : {X1:t -> t -> t} {N1:nat ([x:t] [x1:t] X1 x x1)} plus_min N1 z N1.
plus_min_s :
   {X1:t -> t -> t} {X2:t -> t -> t} {X3:t -> t -> t}
      {N1:nat ([x:t] [x1:t] X1 x x1)} {N2:nat ([x:t] [x1:t] X2 x x1)}
      {N3:nat ([x:t] [x1:t] X3 x x1)}
      plus_min N1 N2 N3 -> plus_min N1 (s N2) (s N3).
%worlds () (plus_min N1 N2 N3).
%total N2 (plus_min N1 N2 N3).
plus-mod2 : (t -> t -> t) -> (t -> t -> t) -> t -> t -> t
   = [s1:t -> t -> t] [s2:t -> t -> t] [even1:t] [odd1:t]
        s1 (s2 even1 odd1) (s2 odd1 even1).
plus :
   {X:t -> t -> t} {Y:t -> t -> t}
      nat ([x:t] [x1:t] X x x1) -> nat ([x:t] [x1:t] Y x x1)
         -> nat ([x:t] [x1:t] X (Y x x1) (Y x1 x)) -> type.
%mode +{X:t -> t -> t} +{Y:t -> t -> t} +{N1:nat ([x:t] [x1:t] X x x1)}
   +{N2:nat ([x:t] [x1:t] Y x x1)} -{N3:nat ([x:t] [x1:t] X (Y x x1) (Y x1 x))}
   (plus N1 N2 N3).
plus_z : {X1:t -> t -> t} {N1:nat ([x:t] [x1:t] X1 x x1)} plus N1 z N1.
plus_s :
   {X1:t -> t -> t} {X2:t -> t -> t} {N1:nat ([x:t] [x1:t] X1 x x1)}
      {N2:nat ([x:t] [x1:t] X2 x x1)}
      {N3:nat ([x:t] [x1:t] X1 (X2 x x1) (X2 x1 x))}
      plus N1 N2 N3 -> plus N1 (s N2) (s N3).
%worlds () (plus N1 N2 N3).
%total N2 (plus N1 N2 N3).
[Closing file /home/www/twelf/hcode/5bbc1b024cc897579871fc26f81ba453]
%% OK %%