% Natural numbers

nat : type.
O : nat.
S : nat -> nat.

% Addition

plus : nat -> nat -> nat -> type.

plus_O : plus O M M.

plus_Sn : plus (S N) M (S R)
	   <- plus N M R.

%mode plus +N +M -R.
%worlds () (plus N M _).
%total N (plus N M _).

%query 1 1 (plus (S (S O)) (S (S (S O))) R).
%query 3 3 (plus N M (S (S O))).


% Zero is a right identity of addition.

O_id : {N : nat} plus N O N -> type.

- : O_id O plus_O.

- : O_id (S N) (plus_Sn PL)
     <- O_id N PL.

%mode O_id +N -P.
%worlds () (O_id N _).
%total N (O_id N _).


% Incrementing the right operand increments the result.

S_inc : plus N M R -> plus N (S M) (S R) -> type.

- : S_inc plus_O plus_O.

- : S_inc (plus_Sn PLUS1) (plus_Sn PLUS2)
     <- S_inc PLUS1 PLUS2.

%mode S_inc +PLUS1 -PLUS2.
%worlds () (S_inc PLUS1 _).
%total PLUS1 (S_inc PLUS1 _).


% Addition is commutative

plus_comm : plus N M R -> plus M N R -> type.

- : plus_comm plus_O PLUS
     <- O_id N PLUS.

- : plus_comm (plus_Sn PLUS1) PLUS3
     <- plus_comm PLUS1 PLUS2
     <- S_inc PLUS2 PLUS3.

%mode plus_comm +PLUS1 -PLUS2.
%worlds () (plus_comm PLUS1 _).
%total PLUS1 (plus_comm PLUS1 _).


% Subtraction

minus : nat -> nat -> nat -> type.

minus_O : minus N O N.

minus_Sn : minus (S N) (S M) R
	    <- minus N M R.


% Subtraction is the inverse of addition.

plus_minus' : plus M N R
	      -> minus R M N
	      -> type.

- : plus_minus' plus_O minus_O.

- : plus_minus' (plus_Sn PLUS) (minus_Sn MINUS)
     <- plus_minus' PLUS MINUS.

%mode plus_minus' +PLUS -MINUS.
%worlds () (plus_minus' PLUS _).
%total PLUS (plus_minus' PLUS _).

plus_minus : plus N M R
	      -> minus R M N
	      -> type.

- : plus_minus PLUS1 MINUS
     <- plus_comm PLUS1 PLUS2
     <- plus_minus' PLUS2 MINUS.

%mode plus_minus +PLUS -MINUS.
%worlds () (plus_minus PLUS _).
%total PLUS (plus_minus PLUS _).