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

Quelle  interval_arith.dep   Sprache: unbekannt

 
/top,interval,proper_arith,safe_arith,IntervalExpr,box,interval_expr,interval_bexpr,simple_bandb,numerical_bandb,interval_bandb,interval_bolzano,interval_sqrt,interval_trig,interval_lnexp,interval_deriv,subinterval_deriv,interval_chain,interval_taylor,interval_io,interval_expr_sqrt,interval_expr_trig,interval_expr_lnexp,strategies4Q,examples4Q,strategies,examples,top_allen,allen_interval,allen_interval_properties
structures/listn,sort_array,for_iterate,array2list,permutations,min_array_def,more_list_props,branch_and_bound,min_seq,sort_seq,max_array_def,below_arrays,seqs,Unit_adt,concat_arrays,stack,sort_seq_lems,Unit,max_seq,permutations_seq,sort_array_def,Maybe
reals/real_fun_preds,factorial,binomial,sigma_below_sub,abs_lems,poly_rew,sign,log_nat,sqrt_approx,sqrt_exists,prelude_aux,root,polynomials,harmonic_polynomials,real_orders,real_fun_ops,sigma_below,RealInt,intervals_real,quad_minmax,quadratic,real_fun_props,sigma_upto,sigma_swap,real_facts,exponent_props,product,sigma,sqrt,sq,sigma_nat
trig_fnd/trig_values,atan_approx,sincos_def,trig_ineq,trig_approx,acos,exp_term,tan_approx,sincos_phase,atan2,asin,trig_extra,trig_basic,tan_quad,sincos_quad,atan,sincos
series/power_series_derivseq,series,power_series,power_series_deriv,taylor_series,power_series_integ,power_series_conv,power_series_deriv_scaf
lnexp_fnd/exp_series,expt,ln_exp,ln_series,convergence_special,exp_approx,ln_approx
analysis/step_fun_def,continuous_functions_props,lim_of_functions,derivatives,sqrt_derivative,integral_chg_var,nth_derivatives,deriv_domain,top_sequences,deriv_domains,integral,step_fun_props,continuous_functions,continuity_interval,indefinite_integral,taylors,integral_split_scaf,restrict2_deriv,inverse_continuous_functions,derivative_props,integral_cont_scaf,integral_diff_doms,interval_minmax,integral_cont,step_fun_scaf,unif_cont_fun,fundamental_theorem,monotone_subsequence,convergence_ops,derivative_inverse,convergence_functions,polynomial_deriv,deriv_domain_def,epsilon_lemmas,composition_continuous,integral_split,derivatives_def,partitions_scaf,continuous_functions_more,integral_step,real_fun_supinf,sequence_props,integral_bounded,chain_rule,integral_pulse,integral_def,integral_prep,lim_of_composition,convergence_sequences,continuity_props,derivatives_alt
finite_sets/func_composition,finite_sets_minmax,finite_sets_inductions,finite_sets_card_eq,finite_sets_below
ints/factorial,div_nat,floor_more,max_below
top:interval,proper_arith,safe_arith,IntervalExpr,box,interval_expr,interval_bexpr,simple_bandb,numerical_bandb,interval_bandb,interval_bolzano,interval_sqrt,interval_trig,interval_lnexp,interval_deriv,subinterval_deriv,interval_chain,interval_taylor,interval_io,interval_expr_sqrt,interval_expr_trig,interval_expr_lnexp,strategies4Q,examples4Q,strategies,examples,top_allen
interval:reals@sq,reals@sigma_nat,ints@div_nat
proper_arith:interval
safe_arith:interval
IntervalExpr:interval,structures@Unit,reals@real_orders
box:interval,structures@listn
interval_expr:IntervalExpr,box,structures@more_list_props
interval_bexpr:interval_expr,structures@Maybe,reals@RealInt
simple_bandb:safe_arith,interval_expr,structures@array2list,structures@Maybe,structures@branch_and_bound
numerical_bandb:safe_arith,interval_expr,structures@array2list,structures@Maybe,reals@real_orders,structures@branch_and_bound,structures@for_iterate
interval_bandb:interval_bexpr,structures@array2list,structures@Maybe,reals@real_orders,structures@branch_and_bound
interval_bolzano:interval,reals@log_nat,reals@sqrt
interval_sqrt:interval,reals@sqrt_approx,safe_arith,proper_arith
interval_trig:trig_fnd@trig_basic,trig_fnd@trig_approx,trig_fnd@trig_ineq,trig_fnd@tan_approx,trig_fnd@atan_approx,trig_fnd@trig_values,interval,safe_arith,proper_arith
interval_lnexp:lnexp_fnd@exp_approx,lnexp_fnd@ln_approx,interval,safe_arith,proper_arith
interval_deriv:interval_sqrt,interval_trig,interval_lnexp,analysis@deriv_domain,interval,analysis@derivatives,analysis@nth_derivatives,analysis@sqrt_derivative,trig_fnd@sincos,trig_fnd@atan
subinterval_deriv:interval_deriv,analysis@deriv_domain
interval_chain:interval,interval_deriv,analysis@chain_rule
interval_taylor:interval,interval_deriv,reals@factorial,analysis@taylors
interval_io:interval
interval_expr_sqrt:interval_expr,interval_sqrt
interval_expr_trig:interval_expr,interval_trig
interval_expr_lnexp:interval_expr,interval_lnexp
strategies4Q:simple_bandb,numerical_bandb,interval_bandb,interval_io,interval_expr_sqrt,reals@abs_lems
examples4Q:strategies4Q
strategies:strategies4Q,interval_expr_trig,interval_expr_lnexp
examples:strategies
top_allen:allen_interval,allen_interval_properties
allen_interval:interval
allen_interval_properties:allen_interval

[ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ]