REDUCE_CONV : conv
STRUCTURE
reduceLib
SYNOPSIS
Performs arithmetic or boolean reduction at all levels possible.
LIBRARY
reduce
DESCRIPTION
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
RED_CONV, REDUCE_RULE, REDUCE_TAC
HOL  Kananaskis-13