Evaluate subexpressions built up from rational literals of type :real, by
proof.
DESCRIPTION
When applied to a term, REAL_RAT_REDUCE_CONV performs a recursive bottom-up
evaluation by proof of subterms built from rational literals of type :real
using the unary operators `--', `inv' and `abs', and the binary
arithmetic (`+', `-', `*', `/', `pow') and relational (`<', `<=',
`>', `>=', `=') operators, as well as propagating literals through
logical operations, e.g. T /\ x <=> x, returning a theorem that the original
and reduced terms are equal.
The permissible rational literals are integer literals (&n or -- &n),
ratios (&p / &q or -- &p / &q), or decimals (#DDD.DDDD or
#DDD.DDDDeNN). Any numeric result is always put in the form &p / &q or
-- &p / &q with q > 1 and p and q sharing no common factor, or simply
&p or -- &p when that is impossible.