Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: divides_lems.pvs Sprache: PVS

Original von: PVS^©

divides_lems: THEORY
%----------------------------------------------------------------------------
%
%  Divisibility
%
%  Author: Rick Butler
%
%  NOTE.  This theory joins the old divisibility theory with the prelude
%         definitions.  If you hate the fact that the prelude definition of divides
%         using x as an integer, you can use divides_rew instead.
%
%----------------------------------------------------------------------------
BEGIN

   n,n1,n2: VAR nat
   m,m1,m2: VAR posnat
   i,j,k,ip,jp: VAR int
   nn,mm,ii,jj,kk: VAR nzint

   divides_rew: LEMMA divides(mm,i) = (EXISTS (k: int): i = mm*k)

   divides_lt: LEMMA i /= 0 IMPLIES divides(mm,i) IMPLIES mm <= abs(i)

   divides_lt_abs: LEMMA divides(mm,ii) IMPLIES abs(mm) <= abs(ii)

   divides_mod: LEMMA divides(m,i) = (mod(i,m) = 0)

   divides_sym: LEMMA divides(mm,ii) = divides(mm,-ii)

   divides_plus : LEMMA divides(mm,i) AND divides(mm,j) IMPLIES divides(mm,i+j)

   divides_plus_1: LEMMA mm > 1 IMPLIES
                           divides(mm,ii) IMPLIES NOT divides(mm,ii+1)

   IMPORTING min_posnat

   lcm(m1,m2): int = min({k: posnat | divides(m1,k) AND divides(m2,k)})

   IMPORTING max_bounded_posnat

   gcd_noem: LEMMA nonempty?({k: posnat | divides(k, i) AND divides(k, j)})

   gcd_prep: LEMMA
      FORALL (i: int, j: {jj: int | i = 0 => jj /= 0}):
        EXISTS (UB: posnat):
        FORALL (y: ({k: posnat | divides(k, i) AND divides(k, j)})):
          y <= UB

END divides_lems

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