Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: eq_mod.pvs Sprache: PVS

Original von: PVS^©

eq_mod: THEORY
%-------------------------------------------------------------------------------

%-------------------------------------------------------------------------------
BEGIN

    p: VAR nat
    a,b,c,d: VAR int
    j,k: VAR int

    IMPORTING ints@primes

    eq_mod(p)(a,b): bool = (EXISTS k: a = k*p + b)

    eq_mod_equiv: LEMMA equivalence?(eq_mod(p))

    eq_mod_mult : LEMMA eq_mod(p)(a,b) AND
                        eq_mod(p)(c,d)
                       IMPLIES
                           eq_mod(p)(a*c,b*d)

    eq_mod_rem  : LEMMA p > 0 IMPLIES eq_mod(p)(j, rem(p)(j))

    IMPORTING ints@gcd

    gcd_is_1: LEMMA prime?(p) AND NOT divides(p,a) IMPLIES
                    gcd(a,p) = 1

    Euclids_30: LEMMA prime?(p) AND divides(p,a*b) IMPLIES
                      divides(p,a) OR divides(p,b)

    eq_mod_cancel: LEMMA prime?(p) AND
                         NOT divides(p, c)
                    IMPLIES
                         eq_mod(p)(a*c,b*c) IMPLIES
                         eq_mod(p)(a,b)

END eq_mod

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