anchor.diff:    let poly_eq p1 p2 =
       forall2 (fun (c1,m1) (c2,m2) -> c1 = c2 && m1 = m2) p1 p2
     
  -  let memx ((p1,h1),(p2,h2)) ppairs =
  -    not (exists (fun ((q1,_),(q2,_)) -> poly_eq p1 q1 && poly_eq p2 q2)
  -                ppairs)
  +  let memx ((p1, h1), (p2, h2)) ppairs = 
  +      not(exists (fun ((q1, _), (q2, _)) -> poly_eq p1 q1 && poly_eq p2 q2) ppairs)
     
     (* ----------------------------------------------------------------------- *)
     (* Buchberger's second criterion.                                          *)
     (* ----------------------------------------------------------------------- *)
     
  -  let criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs =
  -    /// Tests for failure.
  -    let can f x = 
  -        try f x |> ignore; true
  -        with Failure _ -> false
  -
  -    exists (fun g -> not(poly_eq (fst g) p1) && not(poly_eq (fst g) p2) &&
  -                     can (mdiv lcm) (hd(fst g)) &&
  -                     not(memx (align(g,(p1,h1))) (map snd opairs)) &&
  -                     not(memx (align(g,(p2,h2))) (map snd opairs))) basis
  +  let criterion2 basis (lcm, ((p1, h1), (p2, h2))) opairs = 
  +      /// Tests for failure.
  +      let can f x = 
  +          try 
  +              f x |> ignore
  +              true
  +          with
  +          | Failure _ -> false
  +      exists 
  +          (fun g -> 
  +          not(poly_eq (fst g) p1) && not(poly_eq (fst g) p2) && can (mdiv lcm) (hd(fst g)) 
  +          && not(memx (align(g, (p1, h1))) (map snd opairs)) && not(memx (align(g, (p2, h2))) (map snd opairs))) basis
     
     (* ----------------------------------------------------------------------- *)
     (* Test for hitting constant polynomial.                                   *)
  
positive.code:   (* Reduction of a polynomial (always picking largest monomial possible).   *)
    (* ----------------------------------------------------------------------- *)
    
    let rec reduce basis (pol,hist) =
      match pol with
        [] -> (pol,hist)
      | cm::ptl -> try let q,hnew = reduceb cm basis
                       reduce basis (grob_add q ptl,Add(hnew,hist))
                   with Failure _ ->
                       let q,hist' = reduce basis (ptl,hist)
                       cm::q,hist'
    
    (* ----------------------------------------------------------------------- *)
    (* Check for orthogonality w.r.t. LCM.                                     *)
    (* ----------------------------------------------------------------------- *)
    
    let orthogonal l p1 p2 =
      snd l = snd(grob_mmul (hd p1) (hd p2))
    
    (* ----------------------------------------------------------------------- *)
    (* Compute S-polynomial of two polynomials.                                *)
    (* ----------------------------------------------------------------------- *)
    
    let spoly cm ph1 ph2 =
      match (ph1,ph2) with
        ([],h),p -> ([],h)
      | p,([],h) -> ([],h)
      | (cm1::ptl1,his1),(cm2::ptl2,his2) ->
            (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
                      (grob_cmul (mdiv cm cm2) ptl2),
             Add(Mmul(mdiv cm cm1,his1),
                 Mmul(mdiv (minus_num(fst cm),snd cm) cm2,his2)))
    
    (* ----------------------------------------------------------------------- *)
    (* Make a polynomial monic.                                                *)
    (* ----------------------------------------------------------------------- *)
    
    let monic (pol,hist) =
      if pol = [] then (pol,hist) else
      let c',m' = hd pol in
      (map (fun (c,m) -> (c/c',m)) pol,
       Mmul((num_1 / c',map (K 0) m'),hist))
    
    (* ----------------------------------------------------------------------- *)
    (* The most popular heuristic is to order critical pairs by LCM monomial.  *)
  
negative.code:   (* make the same calculation many times. Could add a cache or something.   *)
    (* ----------------------------------------------------------------------- *)
    
    let rec resolve_proof vars prf = 
        match prf with
        | Start(-1) -> []
        | Start m -> [m, [num_1, map (K 0) vars]]
        | Mmul(pol, lin) -> 
            let lis = resolve_proof vars lin
            map (fun (n, p) -> n, grob_cmul pol p) lis
        | Add(lin1, lin2) -> 
            let lis1 = resolve_proof vars lin1
            let lis2 = resolve_proof vars lin2
            let dom = setify(union (map fst lis1) (map fst lis2))
            map (fun n -> 
                let a = defaultArg (assoc n lis1) []
                let b = defaultArg (assoc n lis2) []
                n, grob_add a b) dom
    
    (* ----------------------------------------------------------------------- *)
    (* Run the procedure and produce Weak Nullstellensatz certificate.         *)
    (* ----------------------------------------------------------------------- *)
    
    let grobner_weak vars pols = 
        let cert = resolve_proof vars (grobner_refute pols)
        let l = itlist (itlist(lcm_num << denominator << fst) << snd) cert (num_1)
        l, map (fun (i, p) -> i, map (fun (d, m) -> (l * d, m)) p) cert
    
    (* ----------------------------------------------------------------------- *)
    (* Prove polynomial is in ideal generated by others, using Grobner basis.  *)
    (* ----------------------------------------------------------------------- *)
    
    let grobner_ideal vars pols pol = 
        let pol', h = reduce (grobner pols) (grob_neg pol, Start(-1))
        if pol' <> [] then failwith "grobner_ideal: not in the ideal"
        else resolve_proof vars h
    
    (* ----------------------------------------------------------------------- *)
    (* Produce Strong Nullstellensatz certificate for a power of pol.          *)
    (* ----------------------------------------------------------------------- *)
    
    let grobner_strong vars pols pol = 
        if pol = [] then 1, num_1, []
        else 
            let vars' = (concl <| Choice.get TRUTH) :: vars
            let grob_z = [num_1, 1 :: (map (fun x -> 0) vars)]
            let grob_1 = [num_1, (map (fun x -> 0) vars')]
            let augment = map(fun (c, m) -> (c, 0 :: m))
            let pols' = map augment pols
            let pol' = augment pol
            let allpols = (grob_sub (grob_mul grob_z pol') grob_1) :: pols'
            let l, cert = grobner_weak vars' allpols
            let d = itlist (itlist(max << hd << snd) << snd) cert 0
            let transform_monomial(c, m) = grob_cmul (c, tl m) (grob_pow vars pol (d - hd m))
            let transform_polynomial q = itlist (grob_add << transform_monomial) q []
            let cert' = map (fun (c, q) -> c - 1, transform_polynomial q) (filter (fun (k, _) -> k <> 0) cert)
            d, l, cert'
      
    (* ----------------------------------------------------------------------- *)
    (* Overall parametrized universal procedure for (semi)rings.               *)
  