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/PVS/ints/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 2 kB

Quelle tmod.pvs Sprache: PVS

tmod: THEORY
%------------------------------------------------------------------------
%
% mod function for number theory
%
% This has been defined using "tdiv"
%
% AUTHOR
% ------
%
%   Ricky W. Butler                email: r.w.butler@larc.nasa.gov
%   Mail Stop 130                            fax: (804) 864-4234
%   NASA Langley Research Center           phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%
%
%------------------------------------------------------------------------

BEGIN

  IMPORTING tdiv

  i,k,cc: VAR int
  m: VAR posnat
  n,a,b,c: VAR nat

  j: VAR nonzero_integer

  ml3: LEMMA abs(i -  m * floor(i/m)) < m
  ml4: LEMMA abs(i +  m * floor(-i/m)) < m

  mod(i,j): {k| abs(k) < abs(j)} = i-j*tdiv(i,j)

  mod_even:       LEMMA integer?(i/j) IMPLIES mod(i,j) = 0

  mod_neg:        LEMMA mod(-i,j) = IF integer?(i/j) THEN 0
                                    ELSE j - mod(i,j)
                                    ENDIF

  mod_neg_d:      LEMMA mod(i,-j) = IF integer?(i/j) THEN 0
                                    ELSE mod(i,j) - j
                                    ENDIF

  mod_eq_arg:     LEMMA mod(j,j) = 0

  mod_lt:         LEMMA abs(i) < abs(j) IMPLIES mod(i,j) =
                                  IF sgn(i) = sgn(j) OR i = 0 THEN i
                                  ELSE i + j
                                  ENDIF

  mod_lt_nat:     LEMMA n < m IMPLIES mod(n,m) = n

  mod_sum_pos:    LEMMA mod(i+k*m,m) = mod(i,m)

  mod_sum:        LEMMA mod(i+k*j,j) = mod(i,j)

  mod_it_is:      LEMMA a = b + m*c AND b < m IMPLIES b = mod(a,m)

  mod_zero:       LEMMA mod(0,j) = 0

  mod_0   :       LEMMA mod(0,j) = 0

  mod_one:        LEMMA mod(1,j) = IF abs(j) = 1 THEN 0
                                    ELSIF j > 0 THEN 1
                                    ELSE j + 1
                                    ENDIF

  mod_of_mod:     LEMMA mod(i + mod(k,m), m) = mod(i+k, m)

  mod_pos:        LEMMA mod(i,m) >= 0 AND mod(i,m) < m

  JUDGEMENT mod(i,m) HAS_TYPE below(m)

% ------- connection with prelude rem --------------

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

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

  AUTO_REWRITE+ mod_pos
  AUTO_REWRITE+ mod_0
  AUTO_REWRITE+ mod_eq_arg
  AUTO_REWRITE+ mod_sum_pos
  AUTO_REWRITE+ mod_of_mod
  AUTO_REWRITE+ mod_sum

END tmod

quality93%

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