Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: graph_conn_piece.prf Sprache: PVS

Original von: PVS^©

infinite_primes: THEORY
BEGIN
    IMPORTING ints@divides_lems,
              reals@product_fseq_posnat,
              prime_factorization
    Primes: set[nat] = {n: nat | prime?(n)}

    n: VAR posnat
    prime_divides: LEMMA  NOT prime?(n) AND n > 1 IMPLIES
                                 (EXISTS (p: nat): prime?(p) AND divides(p,n))

    ii: VAR nat
    divides_product: LEMMA FORALL (fs: fseq[posnat]),
                                       (ii: below(length(fs))):
                                 divides(seq(fs)(ii), product(fs))

    primes_infinite: THEOREM NOT is_finite(Primes)

END infinite_primes

¤ Dauer der Verarbeitung: 0.17 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.