| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 581 B |
|
Quelle floor_div_lems.pvsSprache: PVS |
|||||||||||||||
|
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.9 Sekunden (vorverarbeitet am 2026-06-15) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09