SUC_CONV : conv
STRUCTURE
reduceLib
SYNOPSIS
Calculates by inference the successor of a numeral.
LIBRARY
reduce
DESCRIPTION
If
n
is a numeral (e.g.
0
,
1
,
2
,
3
,...), then
SUC_CONV "SUC n"
returns the theorem:
|- SUC n = s
where
s
is the numeral that denotes the successor of the natural number denoted by
n
.
FAILURE
SUC_CONV tm
fails unless
tm
is of the form
"SUC n"
, where
n
is a numeral.
EXAMPLE
#SUC_CONV "SUC 33";; |- SUC 33 = 34
HOL
Kananaskis-13