Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Auth/Guard/ (Lyx Textverarbeitung ^©) Datei vom 16.11.2025 mit Größe 10 kB

eq_mod.pvs Interaktion und
PortierbarkeitPVS

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%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.32Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Normalansicht

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.