n: VAR nat
m: VAR posnat
i,k: VAR int
j: VAR nonzero_integer
x: VAR real
%-------------------- The following are now in the 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 IFF x >= 0 AND x < 1
floor_small_nat: LEMMA n < m IMPLIES floor(n/m) = 0
floor_max : LEMMA floor(n / m) <= n
END floor_more
¤ 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.0.1Bemerkung:
(vorverarbeitet)
¤
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.
