Quellcode-Bibliothek eq_mod.pvs Sprache: 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

quality100%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders