qed for proof

1 files changed, 37 insertions, 2 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index f61cc48c..608b3710 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -242,5 +242,40 @@ Proof.
     field.
     lra.
   }
-  
-Admitted.
+  assert(Rabs alpha0 <= 257/2147483648)%R as alpha0_ABS.
+  { rewrite alpha0_EQ.
+    unfold x0, bd.
+    gappa.
+  }
+  assert (Rabs (x0 - 1 / b1) <= 3/33554432)%R as x0_delta_ABS.
+  { unfold x0.
+    gappa.
+  }
+  set (x0_delta := (x0 - 1 / b1)%R) in *.
+  assert (Rabs ((bd - b1) / b1) <= 1/9007199254740992)%R as bd_delta_ABS.
+  { unfold bd.
+    gappa.
+  }
+  set (bd_delta := ((bd - b1) / b1)%R) in *.
+  set (rnd_alpha0_delta := (round radix2 (FLT_exp (-1074) 53) ZnearestE alpha0 - alpha0)%R) in *.
+  assert (Rabs rnd_alpha0_delta <= 1/75557863725914323419136)%R as rnd_alpha0_delta_ABS.
+  { unfold rnd_alpha0_delta.
+    gappa.
+  }
+  assert (1/18446744073709551616 <= x0 <= 1)%R as x0_RANGE.
+  { unfold x0.
+    gappa.
+  }
+  assert (Rabs (y1 - 1 / b1) <= 49/4503599627370496)%R as y1_delta_ABS.
+  { rewrite y1_EQ.
+    gappa.
+  }
+  assert (Rabs(x1 - y1) <= 1/9007199254740992)%R as x1_delta_ABS.
+  { unfold x1.
+    gappa.
+  }
+  set (y1_delta := (y1 - 1 / b1)%R) in *.
+  set (x1_delta := (x1-y1)%R) in *.
+  unfold approx_inv_thresh.
+  gappa.
+Qed.