Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/0c63bbc65a3c761a5440d48c79ff4cda]
nat : type.
z : nat.
s : nat -> nat.
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).
even : nat -> type.
even-z : even z.
even-s : {N:nat} even N -> even (s (s N)).
plus-zero-id : {N1:nat} plus N1 z N1 -> type.
%mode +{N:nat} -{D:plus N z N} (plus-zero-id N D).
pzidz : plus-zero-id z plus-z.
pzids :
   {N:nat} {D:plus N z N} plus-zero-id N D -> plus-zero-id (s N) (plus-s D).
%worlds () (plus-zero-id _ _).
%total N (plus-zero-id N _).
plus-flip :
   {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus N1 (s N2) (s N3) -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:plus N1 N2 N3} -{D2:plus N1 (s N2) (s N3)}
   (plus-flip D1 D2).
pfz : {X1:nat} {X2:plus z X1 X1} plus-flip X2 plus-z.
pfs :
   {N1:nat} {N2:nat} {N3:nat} {Dplus:plus N1 N2 N3} {DIH:plus N1 (s N2) (s N3)}
      plus-flip Dplus DIH -> plus-flip (plus-s Dplus) (plus-s DIH).
%worlds () (plus-flip _ _).
%total D (plus-flip D _).
plus-commutes :
   {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus N2 N1 N3 -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:plus N1 N2 N3} -{D2:plus N2 N1 N3}
   (plus-commutes D1 D2).
pcz :
   {N1:nat} {D:plus N1 z N1} {X1:plus z N1 N1}
      plus-zero-id N1 D -> plus-commutes X1 D.
pcs :
   {N2:nat} {N1':nat} {N3':nat} {DIH:plus N2 N1' N3'}
      {D:plus N2 (s N1') (s N3')} {Dplus:plus N1' N2 N3'}
      plus-flip DIH D -> plus-commutes Dplus DIH
         -> plus-commutes (plus-s Dplus) D.
%worlds () (plus-commutes _ _).
%total D (plus-commutes D _).
odd : nat -> type.
odd-1 : odd (s z).
odd-s : {N:nat} odd N -> odd (s (s N)).
succ-even : {N:nat} even N -> odd (s N) -> type.
%mode +{N:nat} +{D1:even N} -{D2:odd (s N)} (succ-even D1 D2).
sez : succ-even even-z odd-1.
ses :
   {X1:nat} {EvenA:even X1} {OddA:odd (s X1)}
      succ-even EvenA OddA -> succ-even (even-s EvenA) (odd-s OddA).
%worlds () (succ-even _ _).
%total D (succ-even D _).
succ-odd : {N:nat} odd N -> even (s N) -> type.
%mode +{N:nat} +{D1:odd N} -{D2:even (s N)} (succ-odd D1 D2).
so1 : succ-odd odd-1 (even-s even-z).
sos :
   {X1:nat} {OddA:odd X1} {EvenA:even (s X1)}
      succ-odd OddA EvenA -> succ-odd (odd-s OddA) (even-s EvenA).
%worlds () (succ-odd _ _).
%total D (succ-odd D _).
sum-even-odd :
   {N1:nat} {N2:nat} {N3:nat}
      even N1 -> odd N2 -> plus N1 N2 N3 -> odd N3 -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:even N1} +{D2:odd N2} +{D3:plus N1 N2 N3}
   -{D4:odd N3} (sum-even-odd D1 D2 D3 D4).
seoz : {X1:nat} {OddN2:odd X1} sum-even-odd even-z OddN2 plus-z OddN2.
seos :
   {X1:nat} {X2:nat} {X3:nat} {EvenN1:even X1} {OddN2:odd X2}
      {PlusN1N2N3:plus X1 X2 X3} {OddN3:odd X3}
      sum-even-odd EvenN1 OddN2 PlusN1N2N3 OddN3
         -> sum-even-odd (even-s EvenN1) OddN2 (plus-s (plus-s PlusN1N2N3))
               (odd-s OddN3).
%worlds () (sum-even-odd _ _ _ _).
%total D (sum-even-odd D _ _ _).
sum-odd-even :
   {N1:nat} {N2:nat} {N3:nat}
      odd N1 -> even N2 -> plus N1 N2 N3 -> odd N3 -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:odd N1} +{D2:even N2} +{D3:plus N1 N2 N3}
   -{D4:odd N3} (sum-odd-even D1 D2 D3 D4).
soe1 :
   {X1:nat} {EvenN2:even X1} {OddN3:odd (s X1)} {X2:plus (s z) X1 (s X1)}
      succ-even EvenN2 OddN3 -> sum-odd-even odd-1 EvenN2 X2 OddN3.
soes :
   {X1:nat} {X2:nat} {X3:nat} {OddN1:odd X1} {EvenN2:even X2}
      {PlusN1N2N3:plus X1 X2 X3} {OddN3:odd X3}
      sum-odd-even OddN1 EvenN2 PlusN1N2N3 OddN3
         -> sum-odd-even (odd-s OddN1) EvenN2 (plus-s (plus-s PlusN1N2N3))
               (odd-s OddN3).
%worlds () (sum-odd-even _ _ _ _).
%total D (sum-odd-even D _ _ _).
sum-odd-even :
   {M:nat} {N:nat} {P:nat} odd M -> even N -> plus M N P -> odd P -> type.
%mode +{M:nat} +{N:nat} +{P:nat} +{O:odd M} +{E:even N} +{P1:plus M N P} -{O2:odd P}
   (sum-odd-even O E P1 O2).
soe :
   {N:nat} {M:nat} {P:nat} {E:even N} {O:odd M} {A0:plus N M P} {O0:odd P}
      {A:plus M N P}
      sum-even-odd E O A0 O0 -> plus-commutes A A0 -> sum-odd-even O E A O0.
%worlds () (sum-odd-even _ _ _ _).
%total D (sum-odd-even D _ _ _).
sum-odds :
   {N1:nat} {N2:nat} {N3:nat}
      odd N1 -> odd N2 -> plus N1 N2 N3 -> even N3 -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:odd N1} +{D2:odd N2} +{D3:plus N1 N2 N3}
   -{D4:even N3} (sum-odds D1 D2 D3 D4).
soz :
   {X1:nat} {OddN2:odd X1} {EvenN3:even (s X1)} {X2:plus (s z) X1 (s X1)}
      succ-odd OddN2 EvenN3 -> sum-odds odd-1 OddN2 X2 EvenN3.
sos :
   {X1:nat} {X2:nat} {X3:nat} {OddN1:odd X1} {OddN2:odd X2}
      {PlusN1N2N3:plus X1 X2 X3} {EvenN3:even X3}
      sum-odds OddN1 OddN2 PlusN1N2N3 EvenN3
         -> sum-odds (odd-s OddN1) OddN2 (plus-s (plus-s PlusN1N2N3))
               (even-s EvenN3).
%worlds () (sum-odds _ _ _ _).
%total D (sum-odds D _ _ _).
[Closing file /home/www/twelfwiki/code/0c63bbc65a3c761a5440d48c79ff4cda]
%% OK %%