----------------------------------------------------------------------
REDUCE_CONV                                                (reduceLib)
----------------------------------------------------------------------
REDUCE_CONV : conv

SYNOPSIS
Performs arithmetic or boolean reduction at all levels possible.

LIBRARY
reduce

DESCRIBE
The conversion {REDUCE_CONV} attempts to apply, in bottom-up order to all
suitable redexes, one of the following conversions from the {reduce} library
(only one can succeed):

   ADD_CONV  AND_CONV  BEQ_CONV  COND_CONV
   DIV_CONV  EXP_CONV   GE_CONV    GT_CONV
   IMP_CONV   LE_CONV   LT_CONV   MOD_CONV
   MUL_CONV  NEQ_CONV  NOT_CONV    OR_CONV
   PRE_CONV  SBC_CONV  SUC_CONV

In particular, it will prove the appropriate reduction for an
arbitrarily complicated expression constructed from numerals and the boolean
constants {T} and {F}.

FAILURE
Never fails, but may give a reflexive equation.

EXAMPLE

#REDUCE_CONV "(2=3) = F";;
|- ((2 = 3) = F) = T

#REDUCE_CONV "(100 < 200) => (2 EXP (8 DIV 2)) | (3 EXP ((26 EXP 0) * 3))";;
|- (100 < 200 => 2 EXP (8 DIV 2) | 3 EXP ((26 EXP 0) * 3)) = 16

#REDUCE_CONV "(15 = 16) \/ (15 < 16)";;
|- (15 = 16) \/ 15 < 16 = T

#REDUCE_CONV "0 + x";;
|- 0 + x = 0 + x


SEEALSO
reduceLib.RED_CONV, reduceLib.REDUCE_RULE, reduceLib.REDUCE_TAC.

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