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

Quelle  numbers.dep   Sprache: unbekannt

 
/top,prime_factorization,product_perm_lems,unique_factorization,unique_scaf,infinite_primes,sqrt_two,eq_mod,primes_sum_squares,chinese_remainder,fermats_little_theorem
structures/sort_array,for_iterate,permutations,min_array_def,max_array_def,below_arrays,fseqs,fsq,permutations_fseq,sort_fseq,sort_array_def
reals/binomial_identities,factorial,binomial,sign,sqrt_exists,polynomials,real_fun_ops,sigma_upto,sigma_swap,product_nat,product,sigma,sqrt,product_fseq_posnat,sq,sigma_nat
finite_sets/func_composition,finite_sets_card_eq,finite_sets_below
ints/factorial,div,gcd,divides_lems,floor_div_lems,primes,mod_lems,max_bounded_posnat,gcd_fractions,min_posnat,pigeonhole,abs_rews
top:prime_factorization,unique_factorization,product_perm_lems,infinite_primes,sqrt_two,eq_mod,primes_sum_squares,chinese_remainder,fermats_little_theorem
prime_factorization:ints@primes,reals@product_fseq_posnat,product_perm_lems
product_perm_lems:reals@product_fseq_posnat,structures@permutations_fseq,structures@sort_fseq
unique_factorization:prime_factorization,unique_scaf
unique_scaf:prime_factorization,ints@gcd,structures@fseqs,product_perm_lems
infinite_primes:ints@divides_lems,reals@product_fseq_posnat,prime_factorization
sqrt_two:reals@sqrt,ints@gcd_fractions
eq_mod:ints@primes,ints@gcd
primes_sum_squares:ints@primes,ints@gcd,prime_factorization
chinese_remainder:ints@gcd,reals@product_nat
fermats_little_theorem:ints@mod_lems,ints@primes,eq_mod,reals@factorial,reals@binomial_identities,reals@polynomials

[ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ]