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

Quelle  float.dep   Sprache: unbekannt

 
/top,float,axpy,IEEE_854,IEEE_854_defs,IEEE_854_values,sum_hack,sum_lemmas,enumerated_type_defs,IEEE_854_remainder,real_to_fp,over_under,fp_round_aux,round,IEEE_854_fp_int,arithmetic_ops,comparison1,infinity_arithmetic,NaN_ops,IEEE_link
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,sign,log_nat,sqrt_exists,root,prelude_aux,real_fun_ops,sigma_below,intervals_real,real_fun_props,sigma_upto,real_facts,exponent_props,sigma,sqrt,sq,sigma_nat
series/power_series_derivseq,series,power_series,power_series_deriv,taylor_series,power_series_integ,power_series_conv,power_series_deriv_scaf
lnexp_fnd/expt,ln_exp,ln_series,convergence_special,ln_approx
analysis/step_fun_def,continuous_functions_props,lim_of_functions,derivatives,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,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,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,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,mod_lems,max_below
top:float,axpy,IEEE_854,IEEE_854_defs,infinity_arithmetic,comparison1,NaN_ops,arithmetic_ops,IEEE_854_remainder,IEEE_854_fp_int,real_to_fp,over_under,IEEE_854_values,round,fp_round_aux,sum_lemmas,enumerated_type_defs,sum_hack,IEEE_link
float:lnexp_fnd@ln_exp,lnexp_fnd@expt,lnexp_fnd@ln_approx
axpy:float
IEEE_854:IEEE_854_defs
IEEE_854_defs:IEEE_854_values,IEEE_854_remainder,IEEE_854_fp_int,arithmetic_ops,comparison1,infinity_arithmetic,NaN_ops,enumerated_type_defs,reals@sqrt
IEEE_854_values:sum_hack,sum_lemmas,enumerated_type_defs
sum_hack:
sum_lemmas:sum_hack
enumerated_type_defs:
IEEE_854_remainder:IEEE_854_values,real_to_fp,round
real_to_fp:IEEE_854_values,over_under,fp_round_aux,round
over_under:IEEE_854_values,fp_round_aux,enumerated_type_defs,round
fp_round_aux:round,enumerated_type_defs
round:enumerated_type_defs
IEEE_854_fp_int:IEEE_854_values,real_to_fp,round
arithmetic_ops:IEEE_854_values,real_to_fp,enumerated_type_defs
comparison1:IEEE_854_values
infinity_arithmetic:IEEE_854_values,enumerated_type_defs
NaN_ops:IEEE_854_values,enumerated_type_defs
IEEE_link:ints@mod_lems,IEEE_854,float

[ Dauer der Verarbeitung: 0.19 Sekunden  (vorverarbeitet)  ]