diff --git a/checkerScript.sml b/checkerScript.sml
index 88f2050e0e148de53e3e35065553ea1893ee5127..d66de3ef70b69204a30fde831818ee81ab9bf1f2 100644
--- a/checkerScript.sml
+++ b/checkerScript.sml
@@ -22,6 +22,7 @@ Definition approx_def:
   | _ => ([],0)
 End
 
+
 (**
   Checks that the zero intervals encoded in the certificate actually are
   all of the zeroes of derivative of the difference between the approximated
@@ -39,15 +40,34 @@ End
   Checks that the value at the extrema of the error polynomial are less than or
   equal to the actual error encoded in the certificate **)
 (* TODO: Is this the correct way of checking the zeroes?? Check Harrison paper *)
+
+
+(** In the second part of the definition,
+    the first point line verifies that the zero interval (z1, z2) is inside
+    the large interval vi
+
+    the second point verifies that (z1,z2) is indeed the zero interval by
+    looking at the sign of the values of derivative polynomial at z1 and z2.
+    If (z1, z2) contains the zero of the derivative polynomial, then the
+    product of the values of the derivative polynomial at z1 and z2 < 0
+
+    the third point then verifies that value of polynomial in the extremal
+    points is bounded by eps
+
+    How do we incorporate:
+    Tolerable bound for size of the inteval (z1, z2) i.e. e in the paper
+ **)
 Definition validateZeroesLeqErr_def:
-  validateZeroesLeqErr diffPoly iv [] eps =
-    (if poly diffPoly (FST iv) ≤ eps ∧ poly diffPoly (SND iv) ≤ eps
+  validateZeroesLeqErr diffPoly deriv_poly iv [] eps =
+    (if abs(poly diffPoly (FST iv)) ≤ eps ∧ abs(poly diffPoly (SND iv)) ≤ eps
     then Valid
     else Invalid "Outer points")
   ∧
-  validateZeroesLeqErr diffPoly iv ((z1,z2)::zeroes) eps =
-    (if poly diffPoly z1 ≤ eps ∧ poly diffPoly z2 ≤ eps
-     then validateZeroesLeqErr diffPoly iv zeroes eps
+  validateZeroesLeqErr diffPoly deriv_poly iv ((z1,z2)::zeroes) eps =
+  ( if ((FST iv) < z1 ∧ z2 < (SND iv) ∧ z1 ≤ z2 ∧
+        ((poly deriv_poly z1) * (poly deriv_poly z2) < &0) ∧
+        abs(poly diffPoly z1) ≤ eps ∧ abs(poly diffPoly z2) ≤ eps)
+        then validateZeroesLeqErr diffPoly deriv_poly iv zeroes eps
      else Invalid "Zero of derivate not an extremal point or extrema too big")
 End
 
@@ -72,7 +92,8 @@ Definition checker_def:
           in
             case checkZeroes numZeroes cert.zeroes of
             | Valid =>
-                validateZeroesLeqErr errorp cert.iv cert.zeroes (cert.eps - err)
+                validateZeroesLeqErr errorp deriv
+                                     cert.iv cert.zeroes (cert.eps - err)
             | Invalid s => Invalid s
 End