anchor.diff:    (* 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 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) ->
  +          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
  +          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
  +  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
  +  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'
  +  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.               *)
  
positive.code:   
    let grob_neg = map (fun (c,m) -> (minus_num c,m))
    
    let rec grob_add l1 l2 =
      match (l1,l2) with
        ([],l2) -> l2
      | (l1,[]) -> l1
      | ((c1,m1)::o1,(c2,m2)::o2) ->
            if m1 = m2 then
              let c = c1+c2 
              let rest = grob_add o1 o2 in
              if c = num_0 then rest else (c,m1)::rest
            else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
            else (c2,m2)::(grob_add l1 o2)
    
    let grob_sub l1 l2 = grob_add l1 (grob_neg l2)
    
  
negative.code:   
    let rec grob_cmul cm pol = map (grob_mmul cm) pol
    
    let rec grob_mul l1 l2 = 
        match l1 with
        | [] -> []
        | (h1 :: t1) -> grob_add (grob_cmul h1 l2) (grob_mul t1 l2)
    
    let grob_inv l = 
        match l with
        | [c, vs] when forall (fun x -> x = 0) vs -> 
            if c = num_0 then failwith "grob_inv: division by zero"
            else [num_1 / c, vs]
        | _ -> failwith "grob_inv: non-constant divisor polynomial"
    
    let grob_div l1 l2 = 
        match l2 with
        | [c, l] when forall (fun x -> x = 0) l -> 
            if c = num_0 then failwith "grob_div: division by zero"
            else grob_cmul (num_1 / c, l) l1
        | _ -> failwith "grob_div: non-constant divisor polynomial"
    
    let rec grob_pow vars l n = 
        if n < 0 then failwith "grob_pow: negative power"
        else if n = 0 then [num_1, map (fun v -> 0) vars]
        else grob_mul l (grob_pow vars l (n - 1))
    
    (* ----------------------------------------------------------------------- *)
    (* Monomial division operation.                                            *)
    (* ----------------------------------------------------------------------- *)
    
    let mdiv (c1, m1) (c2, m2) = 
        (c1 / c2, 
         map2 (fun n1 n2 -> 
             if n1 < n2 then failwith "mdiv"
             else n1 - n2) m1 m2)
    
    (* ----------------------------------------------------------------------- *)
    (* Lowest common multiple of two monomials.                                *)
  