nat : type.
z : nat. 
s : nat -> nat.



plus : nat -> nat -> nat -> type.
%mode plus +N1 +N2 -N3.

plus/z : plus z N N.

plus/s : plus (s N1) N2 (s N3) 
          <- plus N1 N2 N3.



plus-zero : {N} plus N z N -> type.
%mode plus-zero +N -D.

plus-zero/z : plus-zero z plus/z.

plus-zero/s : plus-zero (s N) (plus/s D) <- plus-zero N D.



plus-succ : plus N1 N2 N3 -> plus N1 (s N2) (s N3) -> type.
%mode plus-succ +D1 -D2.

plus-succ/z : plus-succ plus/z plus/z.

plus-succ/s : plus-succ (plus/s D1) (plus/s D2)
               <- plus-succ D1 D2.



plus-comm : plus A B C -> plus B A C -> type.
%mode plus-comm +A -B.

plus-comm/z : plus-comm plus/z (D: plus N z N)
               <- plus-zero N D.
plus-comm/s : plus-comm (plus/s D1) D2
               <- plus-comm D1 D3
               <- plus-succ D3 D2.

%solve derivA : plus (s (s z)) (s z) _.
%solve derivB : plus-comm derivA C.

can-plus : {A}{B}{C} plus A B C -> type.
%mode can-plus +A +B -C -D.

can-plus/z : can-plus z B B plus/z.

can-plus/s : can-plus (s A) B (s C) (plus/s D)
              <- can-plus A B C D.

%worlds () (can-plus _ _ _ _).
%total T (can-plus T _ _ _).


can-plus-zero : {N}{D: plus N z N} plus-zero N D -> type.
%mode can-plus-zero +N -D -DZ.

can-plus-zero/z : can-plus-zero z plus/z plus-zero/z.

can-plus-zero/s : can-plus-zero (s N) (plus/s D) (plus-zero/s DZ)
		   <- can-plus-zero N D DZ.

%worlds () (can-plus-zero _ _ _).
%total T (can-plus-zero T _ _).



can-plus-succ : {D:plus A B C}{D': plus A (s B) (s C)} plus-succ D D' -> type.
%mode can-plus-succ +D -D' -DS.

can-plus-succ/z : can-plus-succ plus/z plus/z plus-succ/z.

can-plus-succ/s : can-plus-succ (plus/s D) (plus/s D') (plus-succ/s DS)
		   <- can-plus-succ D D' DS.

%worlds () (can-plus-succ _ _ _).
%total T (can-plus-succ T _ _).


can-plus-comm : {D: plus A B C}{D': plus B A C} plus-comm D D' -> type.
%mode can-plus-comm +D -D' -DC.

can-plus-comm/z : can-plus-comm plus/z (D: plus N z N) (plus-comm/z DZ)
		   <- can-plus-zero N D (DZ: plus-zero N D).

can-plus-succ/s : can-plus-comm (plus/s D) D'' (plus-comm/s DS DC)
		   <- can-plus-comm D D' DC
		   <- can-plus-succ D' D'' DS.

%worlds () (can-plus-comm _ _ _).
%total T (can-plus-comm T _ _).