Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Automaten ueber Termen.unvollendet.pdf Sprache: PVS

Original von: PVS^©

fermats_little_theorem: THEORY
%------------------------------------------------------------------------------
%   Fermat's Little Theorem
%
%   Anthony Narkawicz
%   December 2012
%------------------------------------------------------------------------------
BEGIN

    IMPORTING ints@mod_lems, ints@primes, eq_mod,
              reals@factorial, reals@binomial_identities,
       reals@polynomials

    n,m,p,l: VAR nat
    a,b: VAR nat
    k: VAR int
    np: VAR posnat

    prime_divides_choose: LEMMA
      prime?(p) AND np < p IMPLIES
      divides(p,C(p,np))

    Fermats_Little: THEOREM prime?(p) AND a<p %just for nats
                            IMPLIES
                               eq_mod(p)(a^p,a)

    fermats_little_theorem: THEOREM prime?(p) %just for nats
                            IMPLIES
                               eq_mod(p)(k^p,k)

END fermats_little_theorem

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