| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 574 B |
|
Quelle floor_more.pvs Sprache: PVS |
|||||||||
|
floor_more: THEORY
BEGIN 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 ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28