Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/pvsbin/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 7.10.2014 mit Größe 3 kB image not shown  

Quelle  reals.dep   Sprache: unbekannt

 
/top,top_sigma,sigma,sigma_nat,sigma_posnat,sigma_int,sigma_upto,sigma_below,sigma_below_sub,sigma_fseq_def,sigma_fseq,mixed_products,product,mixed_sigmas,old_sigma,abs_lems,sq,root,binomial,factorial,bound_defs,bounded_reals,reals_complete_more,circles_and_lines,quad_minmax,quadratic,sqrt,sign,sqrt_exists,exponent_props,expt_rew,factorial_props,harmonic_polynomials,log_nat,prelude_aux,base_repr,min_max,polynomials,sigma_swap,real_fun_ops,more_polynomial_props,binomial_identities,poly_rew,bernstein_polynomials,quadratic_2b,convex_functions,real_orders,real_order_ep,real_fun_ops_aux,real_fun_preds,real_fun_orders,real_fun_props,real_sets,real_facts,sign3,sq_rew,sqrt_rew,sqrt_approx,intervals_real,product_below,product_int,product_nat,product_posnat,product_upto,product_seq,product_seq_scaf,product_fseq,product_fseq_posnat,connected_set,RealInt
structures/listn,for_iterate,array2list,more_list_props,fseqs,fsq
ints/factorial
top:top_sigma,mixed_products,mixed_sigmas,old_sigma,abs_lems,binomial,bound_defs,bounded_reals,circles_and_lines,exponent_props,expt_rew,factorial_props,harmonic_polynomials,log_nat,base_repr,min_max,polynomials,more_polynomial_props,poly_rew,bernstein_polynomials,quadratic,quadratic_2b,quad_minmax,convex_functions,real_orders,real_order_ep,reals_complete_more,real_fun_ops,real_fun_ops_aux,real_fun_preds,real_fun_orders,real_fun_props,real_sets,real_facts,sign,sign3,sq,sqrt,sq_rew,sqrt_approx,sqrt_rew,intervals_real,product,product_below,product_int,product_nat,product_posnat,product_upto,product_seq,product_fseq,product_fseq_posnat,connected_set,RealInt
top_sigma:sigma,sigma_nat,sigma_posnat,sigma_int,sigma_upto,sigma_below,sigma_below_sub,sigma_fseq_def,sigma_fseq
sigma:
sigma_nat:sigma
sigma_posnat:sigma
sigma_int:sigma
sigma_upto:sigma
sigma_below:sigma
sigma_below_sub:sigma_below
sigma_fseq_def:sigma_nat,structures@fseqs
sigma_fseq:sigma_fseq_def
mixed_products:product
product:structures@for_iterate
mixed_sigmas:sigma
old_sigma:
abs_lems:sq,root
sq:
root:
binomial:factorial,sigma_upto,product
factorial:ints@factorial,product
bound_defs:
bounded_reals:reals_complete_more
reals_complete_more:bound_defs
circles_and_lines:quad_minmax
quad_minmax:quadratic
quadratic:sqrt,sign
sqrt:sq,sign,sqrt_exists
sign:sq
sqrt_exists:
exponent_props:
expt_rew:
factorial_props:ints@factorial,sqrt
harmonic_polynomials:sq,sigma_nat,binomial
log_nat:prelude_aux
prelude_aux:
base_repr:log_nat,sigma_nat,structures@array2list
min_max:
polynomials:sigma_nat,factorial,binomial,sigma_swap,real_fun_ops
sigma_swap:sigma
real_fun_ops:
more_polynomial_props:polynomials,sign,log_nat,min_max,binomial_identities
binomial_identities:polynomials,binomial
poly_rew:polynomials
bernstein_polynomials:polynomials,sigma_swap,binomial_identities
quadratic_2b:quadratic
convex_functions:quadratic,real_fun_ops
real_orders:
real_order_ep:
real_fun_ops_aux:real_fun_ops,sq
real_fun_preds:
real_fun_orders:
real_fun_props:real_fun_ops,real_fun_preds
real_sets:bounded_reals
real_facts:
sign3:sign,sq
sq_rew:sq
sqrt_rew:sqrt,sq_rew
sqrt_approx:sq,sqrt,log_nat
intervals_real:
product_below:product
product_int:product
product_nat:product
product_posnat:product
product_upto:product
product_seq:product_seq_scaf
product_seq_scaf:
product_fseq:structures@fseqs,product_nat
product_fseq_posnat:structures@fseqs,product_nat
connected_set:
RealInt:

[ Dauer der Verarbeitung: 0.18 Sekunden  (vorverarbeitet)  ]