Quelle  prime_factorization.pvs

prime_factorization: THEORY
BEGIN

   IMPORTING ints@primes

   m: VAR posnat
   N,n: VAR nat


   IMPORTING reals@product_fseq_posnat

   fs: VAR fseq

   prime_factorization: LEMMA FORALL m:
                                (EXISTS fs: m = product(fs) AND
                                   (FORALL (i: below(length(fs))): 
                                           prime?(seq(fs)(i))))



   list_of_primes?(fs): bool = (FORALL (i: below(length(fs))): prime?(seq(fs)(i)))

   IMPORTING product_perm_lems

   ordered_list_of_primes?(fs): bool = list_of_primes?(fs) AND
                                       non_decreasing?(fs)
   
   prime_factors: LEMMA FORALL (m: posnat): 
                            (EXISTS fs: m = product_fseq_posnat.product(fs) AND
                               ordered_list_of_primes?(fs))

END prime_factorization