| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/float/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quellcode-Bibliothek sum_hack.pvs Sprache: PVS |
|||||||||
|
sum_hack % [ parameters ]
: THEORY BEGIN % ASSUMING % assuming declarations % ENDASSUMING %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Some stuff that will eventually be loaded from a library, % once the PVS library mechanism works. i,j,k:var nat F: var [nat->real] Sum(j,F):recursive real = if j=0 then 0 else F(j-1)+Sum(j-1,F) endif measure j F1,F2: var [nat->nonneg_real] Sum_nonneg: lemma Sum(j,F1)>=0 %%%%%%% Modif S. Boldo % JUDGEMENT Sum HAS_TYPE [nat,[nat->nonneg_real]->nonneg_real] %%%%%%% Fin modif Sum_zero: lemma Sum(j,F1)=0 iff forall (i:below(j)): F1(i)=0 Sum_pos: lemma Sum(j,F1)>0 iff (exists (i:below(j)): F1(i)>0) Sum_le: lemma (forall (i:below(j)): F1(i) <= F2(i)) => Sum(j,F1)<=Sum(j,F2) Sum_ge1: lemma (exists (i:below(j)): F1(i)>=1) => Sum(j,F1)>=1 pz: var posreal Sum_ge: lemma (exists (i:below(j)): F1(i)>= pz) => Sum(j,F1)>=pz Sum_split: lemma forall (i:upto(j)): Sum(j,F) = Sum(i,F) + Sum(j-i,lambda k: F(k+i)) END sum_hack ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28