%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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
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.
