Real Numbers

Elementary properties of and operations over real numbers. Main contributions:

a family of summation functions over functions [T FROM int -> real] (see sigma.pvs)
properties on min,max (see min_max.pvs)
additional properties of abs (see abs_lems.pvs)
defines product over functions [int -> real] (see product_real.pvs)
defines sup, inf, max, min (see bounded_reals.pvs)
properties of sup, inf, max, min (see real_sets.pvs)
adding, subtracting, etc on functions (see real_fun_ops.pvs)
increasing?, decreasing?, etc on functions (see real_fun_preds.pvs) and properties (see real_fun_props.pvs)
additional properties of exponent (see exponent_props.pvs)
properties of square root (see sqrt.pvs and sqrt_rew.pvs)
definition of newton and bisection methods for computing square roots (see sqrt_newton and sqrt_bisect in sqrt_approx.pvs)
square function and properties (see sq.pvs and sq_rew.pvs)
properties of sign function (see sign.pvs)
properties of sign3 function (see sign3.pvs)
solution of quadratic equations (see quadratic.pvs)
a better solution of quadratic equations for 2b (see quadratic_2b.pvs)
minimum and Maximum of quadratic equations (see quad_minmax.pvs)
binomial coefficient (see binomial.pvs)
polynomials (see polynomials.pvs)

Highlights

Theorem	Location	PVS Name	Contributors