Quelle 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%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.