NUM_REDUCE_CONV : term -> thm
# NUM_REDUCE_CONV `(432 - 234) + 198`;; val it : thm = |- 432 - 234 + 198 = 396 # NUM_REDUCE_CONV `if 100 < 200 then 2 EXP (8 DIV 2) else 3 EXP ((26 EXP 0) * 3)`;; val it : thm = |- (if 100 < 200 then 2 EXP (8 DIV 2) else 3 EXP (26 EXP 0 * 3)) = 16 # NUM_REDUCE_CONV `(!x. f(x + 2 + 2) < f(x + 0)) ==> f(12 * x) = f(12 * 12)`;; val it : thm = |- (!x. f (x + 2 + 2) < f (x + 0)) ==> f (12 * x) = f (12 * 12) <=> (!x. f (x + 4) < f (x + 0)) ==> f (12 * x) = f 144