% loads of obvious axioms about natural numbers.

nat : type.        %name nat N n.

0 : nat.
s : nat -> nat.

< : nat -> nat -> type.   %infix none 5 <.
%name < LT lt.
lt0 : 0 < (s N).
lts : (s N1) < (s N2) <- N1 < N2.

plus : nat -> nat -> nat -> type.
p0 : plus N 0 N.
ps : plus N (s M) (s X) <- plus N M X.
%mode plus +N +M -X.

minus : nat -> nat -> nat -> type.
m0 : minus N 0 N.
ms : minus (s N) (s M) X <- minus N M X.
%mode minus +N +M -X.
     
pred : nat -> nat -> type.
preds : pred (s N) N.
%mode pred +N -M.

nat-eq : nat -> nat -> type.
nat-eqi : nat-eq N N.
%mode nat-eq +M +N.

minus-eq : minus X Y Z -> minus X Y W -> nat-eq Z W -> type.
%mode minus-eq +M1 +M2 -E.
minus-eq-m0 : minus-eq m0 m0 nat-eqi.
minus-eq-ms : minus-eq (ms M1 : minus (s X) (s Y) Z)
	               (ms M2 : minus (s X) (s Y) W)
	               E
	       <- minus-eq M1 M2 E.

minus-self : {X : nat} minus X X 0 -> type.
%mode minus-self +X -M.
minus-self-0 : minus-self 0 m0.
minus-self-s : minus-self (s X) (ms M) <- minus-self X M.

minus-sfirst : minus X Y Z -> minus (s X) Y (s Z) -> type.
%mode minus-sfirst +M -M'.
minus-sfirst-0 : minus-sfirst m0 m0.
minus-sfirst-s : minus-sfirst (ms M) (ms M') <- minus-sfirst M M'.

succ-eq : nat-eq Q R -> nat-eq (s Q) (s R) -> type.
%mode succ-eq +M -N.
succ-eqi : succ-eq nat-eqi nat-eqi.

plus-zero : plus X 0 Y -> nat-eq X Y -> type.
%mode plus-zero +M -E.
plusz0 : plus-zero p0 nat-eqi.

plus-eq : plus X Y Z -> plus X Y W -> nat-eq Z W -> type.
%mode plus-eq +M1 +M2 -E.
plus-eq-p0 : plus-eq p0 p0 nat-eqi.
plus-eq-ps : plus-eq (ps M1 : plus X (s Y) (s Q))
	              (ps M2 : plus X (s Y) (s R)) EE
    <- plus-eq M1 M2 (E : nat-eq Q R)
    <- succ-eq E (EE : nat-eq (s Q) (s R)).

% if   a + (b + 1) = c   then  (a + 1) + b = c
plus-flip : plus X (s Y) Z -> plus (s X) Y Z -> type.
%mode plus-flip +P -PP.
% by induction on P 
plus-flip0 : plus-flip (ps p0 : plus X (s 0) (s X)) p0.
plus-flips : {P : plus A B E}
	      plus-flip (ps P) PP ->
	      plus-flip (ps (ps P)) (ps PP).

plus-lzero : {X : nat} plus 0 X X -> type.
%mode plus-lzero +X -P.
plus-lz0 : plus-lzero 0 p0.
plus-lzs : plus-lzero (s X) (ps P) <- plus-lzero X P.

plus-commutes : plus X Y Z -> plus Y X Z -> type.
%mode plus-commutes +P -PP.
plus-coms :  plus-flip (ps PP) PPP ->
	     plus-commutes P PP ->
	     plus-commutes (ps P) PPP.
plus-com0 :  plus-lzero X P ->
	     plus-commutes p0 P.

plus-zero-eq : plus 0 X Y -> nat-eq X Y -> type.
plus-zero-0 : plus-zero-eq p0 nat-eqi.
plus-zero-s : plus-zero-eq (ps P) E' <- plus-zero-eq P E <- succ-eq E E'.
%mode plus-zero-eq +P -E.

eq-refl : nat-eq X Y -> nat-eq Y X -> type.
%mode eq-refl +E -E'.
eq-refli : eq-refl nat-eqi nat-eqi.


%worlds () (minus-eq M1 M2 E).
%total [M1 M2] (minus-eq M1 M2 E).

%worlds () (minus-self X M).
%total X (minus-self X _).

%worlds () (minus-sfirst M M').
%total M (minus-sfirst M _).

%worlds () (succ-eq E EE).
%total [E] (succ-eq E EE).

%worlds ()  (plus-eq M1 M2 E).
%total [M2] (plus-eq M1 M2 E).

%worlds () (plus-flip P PP).
%total [P] (plus-flip P PP).

%worlds () (plus-lzero X P).
%total [X] (plus-lzero X P).

%worlds () (plus-commutes P PP).
%total [P] (plus-commutes P PP).

%worlds () (plus-zero P E).
%total [P] (plus-zero P E).

%worlds () (plus-zero-eq P E).
%total P (plus-zero-eq P E).

%worlds () (eq-refl _ _).
%total E (eq-refl E _).