Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: mod_lems.pvs Sprache: PVS

Original von: PVS^©

mod_lems: THEORY
%------------------------------------------------------------------------
% Develops useful lemmas about mod
%
%
% AUTHOR
% ------
%
%   Ricky W. Butler       email: [email protected]
%   Mail Stop 130      fax: (804) 864-4234
%   NASA Langley Research Center    phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%------------------------------------------------------------------------

  BEGIN

%  IMPORTING mod    %% in prelude NOW

  i,j,k: VAR int
  m: VAR posnat
  n,a,b,c,x: VAR nat
  jj: VAR nzint

% The following rule characterizes the property that incrementing
% modulo m wraps around the zero point.

  mod_0           : LEMMA mod(0,jj) = 0

  mod_1           : LEMMA j > 1 IMPLIES mod(1,j) = 1

  mod_by1         : LEMMA mod(i,1) = 0

  mod_to_rem      : LEMMA mod(i,m) = rem(m)(i)

  mod_0_divides   : LEMMA mod(i,jj) = 0 IFF divides(jj,i)

  mod_wrap_around : LEMMA n < m & (c <= m & c >= m-n) =>
                              mod(n+c, m) = n - (m-c)

  mod_wrap2       : LEMMA c < m IMPLIES mod(m+c, m) = c

% Injection-like properties for mod for limited ranges

  mod_inj1        : LEMMA x < m AND n < m AND c < m AND
                       mod(x + n, m) = mod(x + c, m) IMPLIES n = c

  mod_inj2        : LEMMA x < m AND n < m AND c < m AND
                        mod(x - n, m) = mod(x - c, m) IMPLIES n = c

  mod_wrap_inj    : LEMMA
      x < m AND a < m AND b < m AND a > 0
        IMPLIES (mod(x + a, m) = mod(x - b, m)) = (a + b = m)

  kk, vv: VAR nat
  mod_neg_limited : LEMMA 0 <= kk AND  kk < m AND vv < m AND
                      vv - kk < 0 IMPLIES mod(vv - kk,m) = m + vv - kk

  mod_int_quot: LEMMA FORALL (k:nat, n:posnat):
               integer_pred((k-mod(k,n))/n) AND (k-mod(k,n))/n>=0

  floor_div_prod: LEMMA FORALL (n,m:posnat,i:nat):
floor(i / (n*m)) = floor(floor(i / m) / n)

  mod_mult_quot: LEMMA FORALL (n,m:posnat,i:nat):
    mod(i, n * m) = mod(i, m) + m * mod((i - mod(i, m)) / m, n)

  AUTO_REWRITE+ mod_0
  AUTO_REWRITE+ mod_1
  AUTO_REWRITE+ mod_by1
  AUTO_REWRITE+ mod_eq_arg           %% mod(j,j) = 0
  AUTO_REWRITE+ mod_sum              %% mod(i+k*j,j) = mod(i,j)
  AUTO_REWRITE+ mod_of_mod           %% mod(i + mod(k,m), m) = mod(i+k, m)

END mod_lems

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