Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/9012f229ee72d7c649eab582535f3d87]
nat : type.
z : nat.
s : nat -> nat.
plus : nat -> nat -> nat -> type.
%mode +{N1:nat} +{N2:nat} -{N3:nat} (plus N1 N2 N3).
plus/z : {N:nat} plus z N N.
plus/s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
plus-zero : {N:nat} plus N z N -> type.
%mode +{N:nat} -{D:plus N z N} (plus-zero N D).
plus-zero/z : plus-zero z plus/z.
plus-zero/s :
   {N:nat} {D:plus N z N} plus-zero N D -> plus-zero (s N) (plus/s D).
plus-succ :
   {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-succ D1 D2).
plus-succ/z : {X1:nat} plus-succ plus/z plus/z.
plus-succ/s :
   {X1:nat} {X2:nat} {X3:nat} {D1:plus X1 X2 X3} {D2:plus X1 (s X2) (s X3)}
      plus-succ D1 D2 -> plus-succ (plus/s D1) (plus/s D2).
plus-comm : {A:nat} {B:nat} {C:nat} plus A B C -> plus B A C -> type.
%mode +{A:nat} +{B:nat} +{C:nat} +{A1:plus A B C} -{B1:plus B A C} (plus-comm A1 B1).
plus-comm/z : {N:nat} {D:plus N z N} plus-zero N D -> plus-comm plus/z D.
plus-comm/s :
   {X1:nat} {X2:nat} {X3:nat} {D3:plus X1 X2 X3} {D2:plus X1 (s X2) (s X3)}
      {D1:plus X2 X1 X3}
      plus-succ D3 D2 -> plus-comm D1 D3 -> plus-comm (plus/s D1) D2.
%solve 
plus (s (s z)) (s z) X1.
 OK
derivA : plus (s (s z)) (s z) (s (s (s z))) = plus/s (plus/s plus/z).
%solve 
plus-comm derivA C.
 OK
derivB : plus-comm derivA (plus/s plus/z)
   = plus-comm/s (plus-succ/s plus-succ/z)
        (plus-comm/s (plus-succ/s plus-succ/z)
            (plus-comm/z (plus-zero/s plus-zero/z))).
can-plus : {A:nat} {B:nat} {C:nat} plus A B C -> type.
%mode +{A:nat} +{B:nat} -{C:nat} -{D:plus A B C} (can-plus A B C D).
can-plus/z : {B:nat} can-plus z B B plus/z.
can-plus/s :
   {A:nat} {B:nat} {C:nat} {D:plus A B C}
      can-plus A B C D -> can-plus (s A) B (s C) (plus/s D).
%worlds () (can-plus _ _ _ _).
%total T (can-plus T _ _ _).
can-plus-zero : {N:nat} {D:plus N z N} plus-zero N D -> type.
%mode +{N:nat} -{D:plus N z N} -{DZ:plus-zero N D} (can-plus-zero N D DZ).
can-plus-zero/z : can-plus-zero z plus/z plus-zero/z.
can-plus-zero/s :
   {N:nat} {D:plus N z N} {DZ:plus-zero N D}
      can-plus-zero N D DZ -> can-plus-zero (s N) (plus/s D) (plus-zero/s DZ).
%worlds () (can-plus-zero _ _ _).
%total T (can-plus-zero T _ _).
can-plus-succ :
   {A:nat} {B:nat} {C:nat} {D:plus A B C} {D':plus A (s B) (s C)}
      plus-succ D D' -> type.
%mode +{A:nat} +{B:nat} +{C:nat} +{D:plus A B C} -{D':plus A (s B) (s C)}
   -{DS:plus-succ D D'} (can-plus-succ D D' DS).
can-plus-succ/z : {X1:nat} can-plus-succ plus/z plus/z plus-succ/z.
can-plus-succ/s :
   {X1:nat} {X2:nat} {X3:nat} {D:plus X1 X2 X3} {D':plus X1 (s X2) (s X3)}
      {DS:plus-succ D D'}
      can-plus-succ D D' DS
         -> can-plus-succ (plus/s D) (plus/s D') (plus-succ/s DS).
%worlds () (can-plus-succ _ _ _).
%total T (can-plus-succ T _ _).
can-plus-comm :
   {A:nat} {B:nat} {C:nat} {D:plus A B C} {D':plus B A C} plus-comm D D' -> type.
%mode +{A:nat} +{B:nat} +{C:nat} +{D:plus A B C} -{D':plus B A C} -{DC:plus-comm D D'}
   (can-plus-comm D D' DC).
can-plus-comm/z :
   {N:nat} {D:plus N z N} {DZ:plus-zero N D}
      can-plus-zero N D DZ -> can-plus-comm plus/z D (plus-comm/z DZ).
can-plus-succ/s :
   {X1:nat} {X2:nat} {X3:nat} {D':plus X1 X2 X3} {D'':plus X1 (s X2) (s X3)}
      {DS:plus-succ D' D''} {D:plus X2 X1 X3} {DC:plus-comm D D'}
      can-plus-succ D' D'' DS -> can-plus-comm D D' DC
         -> can-plus-comm (plus/s D) D'' (plus-comm/s DS DC).
%worlds () (can-plus-comm _ _ _).
%total T (can-plus-comm T _ _).
twoplus :
   {A:nat} {B:nat} {C:nat} {D:plus A B C} {D':plus B A C} plus-comm D D' -> type.
%mode +{A:nat} +{B:nat} -{C:nat} -{D:plus A B C} -{D':plus B A C}
   -{D'':plus-comm D D'} (twoplus A B C D D' D'').
twoplus/i :
   {A:nat} {B:nat} {C:nat} {D:plus A B C} {D':plus B A C} {DC:plus-comm D D'}
      can-plus-comm D D' DC -> can-plus A B C D -> twoplus A B C D D' DC.
%worlds () (twoplus _ _ _ _ _ _).
%total {} (twoplus _ _ _ _ _ _).
[Closing file /home/www/twelfwiki/code/9012f229ee72d7c649eab582535f3d87]
%% OK %%