----------------------------------------------------------------------
NEGATE_CONV                                                    (Arith)
----------------------------------------------------------------------
NEGATE_CONV : (conv -> conv)

SYNOPSIS
Function for negating the operation of a conversion that proves a formula to
be either true or false.

DESCRIBE
This function negates the operation of a conversion that proves a formula to
be either true or false. For example, if {conv} proves {"t"} to be equal to
{"T"} then {NEGATE_CONV conv} will prove {"~t"} to be {"F"}.

FAILURE
Fails if the application of the conversion to the negation of the formula does
not yield either {"T"} or {"F"}.

EXAMPLE

#ARITH_CONV "!n. 0 <= n";;
|- (!n. 0 <= n) = T

#NEGATE_CONV ARITH_CONV "~(!n. 0 <= n)";;
|- ~(!n. 0 <= n) = F

#NEGATE_CONV ARITH_CONV "?n. ~(0 <= n)";;
|- (?n. ~0 <= n) = F


----------------------------------------------------------------------