| products/Sources/formale Sprachen/VDM/VDMPP/BuslinesPP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 985 B |
|
Quelle sum_lemmas.pvs Sprache: PVS |
|||||||||
|
sum_lemmas [b:above(1)]: THEORY
BEGIN importing sum_hack i: var nat F1: var [nat->nonneg_real] mant_digit_fun: type = {F1| forall i: F1(i)<=(b-1)*b^(-i-1)} d: var mant_digit_fun Sum_pos_less_1: lemma 0<=Sum(i,d) & Sum(i,d)<= 1-b^(-i) floor_Sum_mant: lemma floor(Sum(i,d))=0 END sum_lemmas ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28