Quelle  sum_lemmas.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