|
mod_nat: THEORY
%-----------------------------------------------------------------------
%
% NOTE: Given that "mod" is now defined in the prelude, this "mod" has
% been renamed "nmod"
%
%-----------------------------------------------------------------------
BEGIN
n,k,n1,n2,c: VAR nat
m,mk: VAR posnat
i: VAR int
IMPORTING div_nat
nmod(n,m): below(m) = n - m*div(n,m)
nmod_even : LEMMA integer_pred(n/m) IMPLIES nmod(n,m) = 0
nmod_lt_nat : LEMMA n < m IMPLIES nmod(n,m) = n
nmod_sum : LEMMA n+i*m >= 0 IMPLIES nmod(n+i*m,m) = nmod(n,m)
nmod_sum_nat : LEMMA n1 < m AND n2 < m IMPLIES
nmod(n1+n2,m) = IF n1 + n2 < m THEN n1+n2
ELSE n1 + n2 - m
ENDIF
nmod_it_is : LEMMA n = k + m*c AND k < m IMPLIES k = nmod(n,m)
nmod_zero : LEMMA nmod(0,m) = 0
nmod_one : LEMMA nmod(1,m) = IF m = 1 THEN 0
ELSE 1
ENDIF
nmod_of_nmod : LEMMA nmod(n + nmod(k,m), m) = nmod(n+k, m)
nmod_mult : LEMMA nmod(nmod(n,mk*m),m) = nmod(n,m)
END mod_nat
[ Verzeichnis aufwärts0.18unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
