Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/reals/

Quellcode-Bibliothek

Datei: products/sources/formale Sprachen/PVS/reals/

Seitenstruktur Beweissystem bei der NASA ^©

RealInt.prf
RealInt.pvs
abs_lems.prf
abs_lems.pvs
base_repr.prf
base_repr.pvs
bernstein_polynomials.prf
bernstein_polynomials.pvs
binomial.prf
binomial.pvs
binomial_identities.prf
binomial_identities.pvs
bound_defs.pvs
bounded_reals.prf
bounded_reals.pvs
circles_and_lines.prf
circles_and_lines.pvs
connected_set.prf
connected_set.pvs
convex_functions.prf
convex_functions.pvs
exponent_props.prf
exponent_props.pvs
expt_rew.prf
expt_rew.pvs
factorial.prf
factorial.pvs
factorial_props.prf
factorial_props.pvs
harmonic_polynomials.prf
harmonic_polynomials.pvs
intervals_real.prf
intervals_real.pvs
log_nat.prf
log_nat.pvs
min_max.prf
min_max.pvs
mixed_products.prf
mixed_products.pvs
mixed_sigmas.prf
mixed_sigmas.pvs
more_polynomial_props.prf
more_polynomial_props.pvs
old_sigma.prf
old_sigma.pvs
poly_rew.prf
poly_rew.pvs
polynomials.prf
polynomials.pvs
prelude_aux.prf
prelude_aux.pvs
product.prf
product.pvs
product_below.prf
product_below.pvs
product_fseq.prf
product_fseq.pvs
product_fseq_posnat.prf
product_fseq_posnat.pvs
product_int.prf
product_int.pvs
product_nat.prf
product_nat.pvs
product_posnat.prf
product_posnat.pvs
product_seq.prf
product_seq.pvs
product_seq_scaf.prf
product_seq_scaf.pvs
product_upto.prf
product_upto.pvs
pvs-attachments
pvs-strategies
quad_minmax.prf
quad_minmax.pvs
quadratic.prf
quadratic.pvs
quadratic_2b.prf
quadratic_2b.pvs
real_facts.prf
real_facts.pvs
real_fun_ops.prf
real_fun_ops.pvs
real_fun_ops_aux.prf
real_fun_ops_aux.pvs
real_fun_orders.pvs
real_fun_preds.prf
real_fun_preds.pvs
real_fun_props.prf
real_fun_props.pvs
real_order_ep.prf
real_order_ep.pvs
real_orders.prf
real_orders.pvs
real_sets.prf
real_sets.pvs
reals_complete_more.prf
reals_complete_more.pvs
root.prf
root.pvs
sigma.prf
sigma.pvs
sigma_below.prf
sigma_below.pvs
sigma_below_sub.prf
sigma_below_sub.pvs
sigma_fseq.prf
sigma_fseq.pvs
sigma_fseq_def.prf
sigma_fseq_def.pvs
sigma_int.prf
sigma_int.pvs
sigma_nat.prf
sigma_nat.pvs
sigma_posnat.prf
sigma_posnat.pvs
sigma_swap.prf
sigma_swap.pvs
sigma_upto.prf
sigma_upto.pvs
sign.prf
sign.pvs
sign3.prf
sign3.pvs
sq.prf
sq.pvs
sq_rew.pvs
sqrt.prf
sqrt.pvs
sqrt_approx.prf
sqrt_approx.pvs
sqrt_exists.prf
sqrt_exists.pvs
sqrt_rew.prf
sqrt_rew.pvs
top.pvs
top_sigma.pvs