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

Quelle  series.dep   Sprache: unbekannt

 
/top,series,series_lems,series_aux,absconv_series,power_series,trig_fun,power_series_conv,trig_props,power_series_deriv,power_series_deriv_scaf,power_series_derivseq,taylor_series,power_series_integ
structures/sort_array,permutations,min_array_def,min_seq,sort_seq,max_array_def,below_arrays,seqs,concat_arrays,sort_seq_lems,max_seq,permutations_seq,sort_array_def
reals/real_fun_preds,sigma_below_sub,abs_lems,root,real_fun_ops,sigma_below,intervals_real,real_fun_props,sigma_upto,real_facts,exponent_props,sigma,sq,sigma_nat
orders/relations_extra,bounded_orders,minmax_orders,well_nat
analysis/step_fun_def,continuous_functions_props,lim_of_functions,derivatives,nth_derivatives,deriv_domain,top_sequences,integral,step_fun_props,continuous_functions,continuity_interval,taylors,indefinite_integral,integral_split_scaf,derivative_props,integral_cont_scaf,interval_minmax,integral_cont,step_fun_scaf,unif_cont_fun,fundamental_theorem,monotone_subsequence,convergence_ops,convergence_functions,deriv_domain_def,epsilon_lemmas,integral_split,derivatives_def,partitions_scaf,continuous_functions_more,integral_step,real_fun_supinf,sequence_props,integral_bounded,integral_pulse,integral_def,integral_prep,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,max_below
top:series,series_lems,series_aux,absconv_series,power_series,trig_fun,trig_props,taylor_series,power_series_deriv,power_series_integ
series:analysis@convergence_ops,reals@sigma_nat
series_lems:series,orders@well_nat
series_aux:series,orders@well_nat
absconv_series:series_lems
power_series:series,ints@factorial,reals@exponent_props
trig_fun:power_series_conv,ints@factorial,analysis@deriv_domain
power_series_conv:power_series,analysis@deriv_domain_def
trig_props:power_series_deriv,trig_fun,analysis@derivative_props,analysis@deriv_domain
power_series_deriv:analysis@deriv_domain_def,power_series_deriv_scaf,power_series_derivseq,analysis@taylors,analysis@nth_derivatives
power_series_deriv_scaf:analysis@deriv_domain_def,power_series_derivseq,analysis@taylors
power_series_derivseq:analysis@deriv_domain_def,power_series_conv,analysis@derivatives
taylor_series:analysis@deriv_domain_def,power_series_deriv
power_series_integ:analysis@deriv_domain_def,power_series_conv,analysis@derivatives,analysis@taylors,power_series_deriv,analysis@integral,analysis@fundamental_theorem,analysis@indefinite_integral

[ Dauer der Verarbeitung: 0.10 Sekunden  (vorverarbeitet)  ]