|
unique_factorization: THEORY
BEGIN
IMPORTING prime_factorization, unique_scaf
fs,fs1,fs2: VAR fseq[posnat]
n,m: VAR nat
i,j: VAR int
FTL_sym: LEMMA (FORALL (k: nat):
k < j
IMPLIES
(FORALL (fs1: fseq[posnat], fs2: fseq[posnat]):
k = product(fs1)
AND k = product(fs2)
AND ordered_list_of_primes?(fs1)
AND ordered_list_of_primes?(fs2) AND k > 1
IMPLIES fs1 = fs2))
AND j = product(fs1)
AND j = product(fs2)
AND ordered_list_of_primes?(fs1)
AND ordered_list_of_primes?(fs2)
AND j > 1
AND length(fs2) > 1
AND length(fs1) > 1
AND seq(fs2)(length(fs2) - 1) < seq(fs1)(length(fs1) - 1)
IMPLIES
fs1 = fs2
FTL_prep: THEOREM n = product(fs1) AND n = product(fs2)
AND ordered_list_of_primes?(fs1)
AND ordered_list_of_primes?(fs2)
AND n > 1
IMPLIES fs1 = fs2
Fundamental_Theorem_Arithmetic: THEOREM n = product(fs1) AND n = product(fs2)
AND ordered_list_of_primes?(fs1)
AND ordered_list_of_primes?(fs2)
IMPLIES fs1 = fs2
END unique_factorization
¤ Dauer der Verarbeitung: 0.18 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.
|
