| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 131 kB |
|
SSL unique_scaf.pvs Sprache: 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) ¤*© Formatika GbR, Deutschland |
|
2026-03-28