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