Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: CoLoR.nix Sprache: PVS

Original von: PVS^©

div_nat: THEORY
%------------------------------------------------------------------------
% Defines natural division:
%
%    Author:   Rick Butler                NASA Langley Research Center
%
% NOTE.  See div library for division defined over the integers
%
%------------------------------------------------------------------------

BEGIN

  IMPORTING floor_more

  n,k: VAR nat
  m: VAR posnat
  i: VAR int

  div(n,m): upto(n) = floor(n/m)

  div_nat      : LEMMA div(n,m) = IF n < m THEN 0 ELSE 1 + div(n-m,m) ENDIF

  div_value    : LEMMA n >= k*m AND n < (k+1)*m IMPLIES div(n,m) = k

  div_sum_nat  : LEMMA n + i*m >= 0 IMPLIES div(n+i*m,m) = div(n,m) + i

  div_multiple : LEMMA div(k*m,m) = k

  div_is_0     : LEMMA div(n,m) = 0 IFF n < m

% ------------ some order relationships -------------

  div_smaller  : LEMMA m * div(n,m) <= n

  div_rem_small: LEMMA n - m * div(n,m) < m

  div_mult_lt  : LEMMA n < k*m IFF div(n,m) < k

% ------------ Special arguments ------------

  div_by_one   : LEMMA div(n,1) = n

  div_zero     : LEMMA div(0,m) = 0

  div_eq_arg   : LEMMA div(m,m) = 1

  div_one      : LEMMA m > 1 IMPLIES div(1,m) = 0

  div_even     : LEMMA integer_pred(n/m) IMPLIES n - m*div(n,m) = 0

END div_nat

¤ 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.