Using nat-less with %reduces

This is an extension of the example given in the %reduces article. The theorem nat-plus-reduces-s is used in conjunction with some standard properties about addition over the natural numbers to show nat-less-reduces, which allows nat-less to be used in termination arguments about other metatheorems.

nat : type.

nat/z	: nat.
nat/s	: nat -> nat.



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

nat-plus/z	: nat-plus nat/z N N.

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



nat-plus-reduces-s	: {N2}{N3}
			   nat-plus (nat/s N1) N2 N3
			   -> type.
%mode nat-plus-reduces-s +D1 +D2 +D3.

-	: nat-plus-reduces-s _ _ (nat-plus/s nat-plus/z).

-	: nat-plus-reduces-s _ _ (nat-plus/s DL)
	   <- nat-plus-reduces-s _ _ DL.

%worlds () (nat-plus-reduces-s _ _ _).
%reduces N2 < N3 (nat-plus-reduces-s N2 N3 _).
%total {D1} (nat-plus-reduces-s _ _ D1).



nat-less-plus	: nat-less N1 N2
		   -> nat-plus N1 (nat/s _) N2
		   -> type.
%mode nat-less-plus +D1 -D2.


-	: nat-less-plus nat-less/z nat-plus/z.

-	: nat-less-plus (nat-less/s DL) (nat-plus/s DP)
	   <- nat-less-plus DL DP.

%worlds () (nat-less-plus _ _).
%total {D1} (nat-less-plus D1 _).



nat-plus-z	: {N}
		   nat-plus N nat/z N
		   -> type.
%mode nat-plus-z +D1 -D2.

-	: nat-plus-z nat/z nat-plus/z.

-	: nat-plus-z _ (nat-plus/s DP)
	   <- nat-plus-z _ DP.

%worlds () (nat-plus-z _ _).
%total {D1} (nat-plus-z D1 _).



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

-	: nat-plus-s nat-plus/z nat-plus/z.

-	: nat-plus-s (nat-plus/s DP1) (nat-plus/s DP2)
	   <- nat-plus-s DP1 DP2.

%worlds () (nat-plus-s _ _).
%total {D1} (nat-plus-s D1 _).



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

-	: nat-plus-commute nat-plus/z DP
	   <- nat-plus-z _ DP.

-	: nat-plus-commute (nat-plus/s DP1) DP2
	   <- nat-plus-commute DP1 DP1'
	   <- nat-plus-s DP1' DP2.

%worlds () (nat-plus-commute _ _).
%total {D1} (nat-plus-commute D1 _).



nat-less-reduces	: {N1}{N2}
			   nat-less N1 N2
			   -> type.
%mode nat-less-reduces +D1 +D2 +D3.

-	: nat-less-reduces _ _ DL
	   <- nat-less-plus DL DP
	   <- nat-plus-commute DP DP'
	   <- nat-plus-reduces-s _ _ DP'.

%worlds () (nat-less-reduces _ _ _).
%reduces N1 < N2 (nat-less-reduces N1 N2 _).
%total {} (nat-less-reduces _ _ _).