Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: unique_scaf.pvs Sprache: PVS

Original von: PVS^©

unique_scaf: THEORY
BEGIN

   IMPORTING prime_factorization, ints@gcd,
             structures@fseqs[posnat]

   fs,fs1,fs2: VAR fseq[posnat]

   n,m: VAR nat
   i,j: VAR int
   p  : VAR (prime?)

   AUTO_REWRITE+ product_eq_arg

   gcd_primes: LEMMA prime?(i) AND prime?(j) AND (i /= 0 OR j /= 0) AND i /= j
                     IMPLIES gcd(i,j) = 1

   len1: LEMMA ordered_list_of_primes?(fs)
                  AND product(fs) = 1 IMPLIES length(fs) = 0

   len3: LEMMA ordered_list_of_primes?(fs)
                     AND length(fs) > 0 IMPLIES  product(fs) > 1

%% The following produces unprovable TCCs for some bizarre reason
%%
%%   seq_eq_len: LEMMA m < length(fs1) AND n < length(fs2)
%%                     AND fs1 ^ (0, m) = fs2 ^ (0, n) IMPLIES m = n

   ordered_list_of_primes_caret: LEMMA FORALL (n: below(length(fs))):
                            ordered_list_of_primes?(fs) IMPLIES
                                 ordered_list_of_primes?(fs ^ (0, n))

   IMPORTING product_perm_lems

   k,pn: VAR posnat
   olop: LEMMA k = pn * m AND prime?(pn) IMPLIES
                  (EXISTS (fs: fseq[posnat]):
                       k = product(fs) AND
                       ordered_list_of_primes?(fs) AND
                       (EXISTS (i: below(length(fs))): seq(fs)(i) = pn))

   product_len_eq: LEMMA product(fs1) = product(fs2) AND
                        ordered_list_of_primes?(fs1) AND
                        ordered_list_of_primes?(fs2) AND
                        length(fs1) = 1
                          IMPLIES length(fs2) = 1

END unique_scaf

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.