NEQ_CONV : conv

- STRUCTURE
- SYNOPSIS
- Proves equality or inequality of two numerals.
- LIBRARY
- reduce
- DESCRIPTION
- If m and n are both numerals (e.g. 0, 1, 2, 3,...), then NEQ_CONV "m = n" returns the theorem:if m and n are identical, or
|- (m = n) = T

if m and n are distinct.|- (m = n) = F

- FAILURE
- NEQ_CONV tm fails unless tm is of the form "m = n", where m and n are numerals.
- EXAMPLE
#NEQ_CONV "12 = 12";; |- (12 = 12) = T #NEQ_CONV "14 = 25";; |- (14 = 25) = F

HOL Kananaskis-14