NEQ_CONV

reduceLib.NEQ_CONV : conv

Proves equality or inequality of two numerals.

If m and n are both numerals (e.g. 0, 1, 2, 3,…), then NEQ_CONV "m = n" returns the theorem:

   |- (m = n) = T

if m and n are identical, or

   |- (m = n) = F

if m and n are distinct.

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