|
floor_div_lems: THEORY
BEGIN
i,k: VAR int
j: VAR nonzero_integer
x: VAR real
%-------------------- following now in prelude --------------------
%
% floor_val: LEMMA i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k
%
% floor_small: LEMMA abs(i) < abs(j) IMPLIES
% floor(i/j) = IF i/j >= 0 THEN 0 ELSE -1 ENDIF
%
% floor_eq_0: LEMMA floor(x) = 0 IMPLIES x >= 0 AND x < 1
n: VAR nat
m: VAR posnat
floor_small_nat: LEMMA n < m IMPLIES floor(n/m) = 0
is_multiple: LEMMA integer_pred(i/j) = (EXISTS k: i = k*j)
END floor_div_lems
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
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.
|
