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.