Library comput1

Require Export alpha.
Require Export Why2Gappa.
Require Export WhyFloatsStrictLegacy.

Local Coercion FtoRradix: Float.float >-> R.

Lemma epik_one_step_FPerrorr: forall (a dres dp dipk dik dimk dikm t t' t1 t2 t3 t4 t5:double),
  (0%Z <= double_value a)%R -> (double_value a <= 1%Z)%R ->
  (0%Z < double_exact a)%R -> (double_exact a <= 1%Z)%R ->
  (Rle (double_round_error a) (powerRZ (IZR 2) (- 49))) ->
  (Rabs (double_value dipk) <= 2%Z)%R -> (Rabs (double_value dik) <= 2%Z)%R ->
  (Rabs (double_value dimk) <= 2%Z)%R -> (Rabs (double_value dikm) <= 2%Z)%R ->
   double_value t = 2%R -> double_value t' = 2%R ->
  (mul_double_post nearest_even t dik t1) ->
  (sub_double_post nearest_even dipk t1 t2) ->
  (add_double_post nearest_even t2 dimk dp) ->
  (mul_double_post nearest_even t' dik t3) ->
  (sub_double_post nearest_even t3 dikm t4) ->
  (mul_double_post nearest_even a dp t5) ->
  (add_double_post nearest_even t4 t5 dres) ->

  (Rabs ( double_value dres - (2 * double_value dik - double_value dikm+ double_exact a *
     (double_value dipk - 2 * double_value dik +double_value dimk)))
     <= 78* powerRZ 2 (-52))%R.

Lemma epik_step1_FPerrorr: forall (a dres dp dipk dik dimk t t1 t2 t3 t4 t5:double),
  (0%Z <= double_value a)%R -> (double_value a <= 1%Z)%R ->
  (0%Z < double_exact a)%R -> (double_exact a <= 1%Z)%R ->
  (Rle (double_round_error a) (powerRZ (IZR 2) (- 49))) ->
  (Rabs (double_value dipk) <= 2%Z)%R -> (Rabs (double_value dik) <= 2%Z)%R ->
  (Rabs (double_value dimk) <= 2%Z)%R ->
  double_value t = 2 ->
  double_value t1 = (5/10)%R ->
  (mul_double_post nearest_even t dik t2) ->
  (sub_double_post nearest_even dipk t2 t3) ->
  (add_double_post nearest_even t3 dimk dp) ->
  (mul_double_post nearest_even t1 a t4) ->
  (mul_double_post nearest_even t4 dp t5) ->
  (add_double_post nearest_even dik t5 dres) ->

  (Rabs ( double_value dres - (double_value dik + /2*double_exact a *
     (double_value dipk - 2 * double_value dik +double_value dimk)))
     <= 81* powerRZ 2 (-53))%R.