LE_CONV : conv

- STRUCTURE
- SYNOPSIS
- Proves result of less-than-or-equal-to ordering on two numerals.
- LIBRARY
- reduce
- DESCRIPTION
- If m and n are both numerals (e.g. 0, 1, 2, 3,...), then LE_CONV "m <= n" returns the theorem:if the natural number denoted by m is less than or equal to that denoted by n, or
|- (m <= n) = T

otherwise.|- (m <= n) = F

- FAILURE
- LE_CONV tm fails unless tm is of the form "m <= n", where m and n are numerals.
- EXAMPLE
#LE_CONV "12 <= 198";; |- 12 <= 198 = T #LE_CONV "46 <= 46";; |- 46 <= 46 = T #LE_CONV "13 <= 12";; |- 13 <= 12 = F

HOL Kananaskis-14