|
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.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
