SBC_CONV : conv

- STRUCTURE
- SYNOPSIS
- Calculates by inference the difference of two numerals.
- LIBRARY
- reduce
- DESCRIPTION
- If m and n are numerals (e.g. 0, 1, 2, 3,...), then SBC_CONV "m - n" returns the theorem:where s is the numeral that denotes the difference of the natural numbers denoted by m and n.
|- m - n = s

- FAILURE
- SBC_CONV tm fails unless tm is of the form "m - n", where m and n are numerals.
- EXAMPLE
#SBC_CONV "25 - 30";; |- 25 - 30 = 0 #SBC_CONV "200 - 200";; |- 200 - 200 = 0 #SBC_CONV "60 - 17";; |- 60 - 17 = 43

HOL Kananaskis-14