Calculates by inference the predecessor of a numeral.
LIBRARY
reduce
DESCRIPTION
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