PRE_CONV
reduceLib.PRE_CONV : conv
Calculates by inference the predecessor of a numeral.
If n is a numeral (e.g. 0, 1, 2, 3,...), then
PRE_CONV "PRE n" returns the theorem:
|- PRE n = s
where s is the numeral that denotes the predecessor of the natural
number denoted by n.
Failure
PRE_CONV tm fails unless tm is of the form ``PRE n``, where
n is a numeral.
Example
> PRE_CONV ``PRE 0``;
val it = |- PRE 0 = 0 : thm
> PRE_CONV ``PRE 1``;
val it = |- PRE 1 = 0 : thm
> PRE_CONV ``PRE 22``;
val it = |- PRE 22 = 21 : thm