diff options
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index d16417fb..f20efa4e 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -499,7 +499,7 @@ Proof. lia. Qed. -Definition rough_approx_div_thresh := 1%R. +Definition rough_approx_div_thresh := 1683627180032%R. Theorem rough_approx_div_longu_correct : forall a b, @@ -607,4 +607,7 @@ Proof. assert (Rabs (rd (rd (IZR a') * f_r) - rd (IZR a') * f_r) <= 1024)%R as DELTA2. { unfold rd. gappa. } set (delta2 := (rd (rd (IZR a') * f_r) - rd (IZR a') * f_r)%R) in *. -Admitted. + unfold rough_approx_inv_thresh in C1D. + set (delta3 := (f_r - 1 / IZR b')%R) in *. + gappa. +Qed. |