|
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.1 Sekunden
(vorverarbeitet)
¤
|
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.
|
