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

Quelle  trig_fnd.dep   Sprache: unbekannt

 
/top,trig_doc,trig,trig_basic,sincos_def,sincos_phase,sincos_quad,acos,asin,atan,tan_quad,atan_approx,trig_values,trig_ineq,trig_full,trig_extra,atan2,trig_approx,exp_term,sincos,tan_approx,law_cosines,trig_degree,trig_inverses,trig_rew,atan_values,atan2_props,jatan2,deriv_sincos,to2pi,integral_sincos,integral_indef_sincos
structures/sort_array,for_iterate,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,factorial,binomial,poly_rew,abs_lems,sigma_below_sub,sign,sqrt_exists,polynomials,root,harmonic_polynomials,real_fun_ops,sigma_below,intervals_real,quadratic,real_fun_props,sigma_upto,sigma_swap,min_max,real_facts,product,sigma,sqrt,sq,sigma_nat
analysis/step_fun_def,continuous_functions_props,lim_of_functions,derivatives,sqrt_derivative,derivatives_lam,nth_derivatives,deriv_domain,top_sequences,deriv_domains,integral,step_fun_props,continuous_functions,continuity_interval,taylors,restrict2_deriv,integral_split_scaf,indefinite_integral,inverse_continuous_functions,derivative_props,integral_cont_scaf,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,chain_rule,integral_bounded,integral_pulse,integral_def,integral_prep,continuous_lambda,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,max_below
top:trig_doc,trig,trig_full,trig_basic,trig_values,trig_ineq,trig_extra,exp_term,trig_approx,tan_approx,atan_approx,law_cosines,trig_degree,trig_inverses,trig_rew,acos,asin,atan,atan_values,atan2,atan2_props,jatan2,to2pi,sincos_phase,sincos,sincos_quad,deriv_sincos,integral_sincos,integral_indef_sincos,tan_quad
trig_doc:
trig:trig_basic,trig_values,trig_ineq
trig_basic:reals@sqrt,sincos_def,atan_approx
sincos_def:sincos_phase,tan_quad
sincos_phase:sincos_quad
sincos_quad:acos,analysis@deriv_domain,analysis@indefinite_integral,analysis@deriv_domains
acos:asin
asin:reals@sq,reals@sqrt,atan,analysis@sqrt_derivative,analysis@derivative_props,analysis@deriv_domains
atan:reals@sq,reals@sigma,reals@sqrt,reals@poly_rew,analysis@derivatives,analysis@restrict2_deriv,analysis@deriv_domains,analysis@fundamental_theorem,analysis@chain_rule,analysis@derivative_props,analysis@continuous_functions_props,analysis@integral,reals@factorial,analysis@nth_derivatives,analysis@taylors,reals@harmonic_polynomials,analysis@polynomial_deriv,reals@binomial,analysis@indefinite_integral
tan_quad:sincos_quad
atan_approx:atan,sincos_def
trig_values:trig_ineq
trig_ineq:trig_basic
trig_full:trig,trig_basic,trig_values,trig_ineq,trig_extra,trig_approx,tan_approx,atan_approx,law_cosines,trig_degree,trig_inverses,trig_rew,asin,acos,atan,atan_values,atan2,atan2_props,jatan2,sincos_phase,sincos,sincos_quad,tan_quad,deriv_sincos
trig_extra:trig_basic,trig_values,trig_ineq,atan2
atan2:trig_basic,atan,asin,acos
trig_approx:exp_term,sincos,trig_ineq,reals@sigma_nat,analysis@derivatives,trig_extra,analysis@derivative_props,analysis@deriv_domains
exp_term:reals@factorial
sincos:reals@quadratic,trig_basic,analysis@deriv_domain,analysis@deriv_domains
tan_approx:trig_approx
law_cosines:trig_basic,atan2
trig_degree:trig_basic,trig_approx,trig_ineq
trig_inverses:trig_basic,asin,acos,atan,atan2
trig_rew:trig_basic
atan_values:atan,trig_values,trig_inverses
atan2_props:atan2,trig_ineq,trig_values,atan_values
jatan2:trig_values,trig_inverses,atan2_props
deriv_sincos:analysis@deriv_domain,sincos,analysis@chain_rule,analysis@composition_continuous,analysis@derivatives_lam
to2pi:atan2,trig_ineq
integral_sincos:analysis@deriv_domain,deriv_sincos,analysis@fundamental_theorem
integral_indef_sincos:analysis@deriv_domain_def,sincos,deriv_sincos,analysis@fundamental_theorem,analysis@chain_rule,analysis@composition_continuous,analysis@continuous_lambda,analysis@derivatives_lam,analysis@indefinite_integral

[ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ]