anchor.diff:  (* ------------------------------------------------------------------------- *)
   
   /// Eliminates predecessor, cutoff subtraction, even and odd, division and modulus.
  -let NUM_SIMPLIFY_CONV =
  -  let pre_tm = (parse_term @"PRE")
  -  let div_tm = (parse_term @"(DIV):num->num->num")
  -  let mod_tm = (parse_term @"(MOD):num->num->num")
  -  let p_tm = (parse_term @"P:num->bool") 
  -  let n_tm = (parse_term @"n:num") 
  -  let m_tm = (parse_term @"m:num")
  -  let q_tm = (parse_term @"P:num->num->bool") 
  -  let a_tm = (parse_term @"a:num") 
  -  let b_tm = (parse_term @"b:num") in
  -  let is_pre tm = is_comb tm && Choice.get <| rator tm = pre_tm
  -  let is_sub = is_binop (parse_term @"(-):num->num->num")
  -  let is_divmod =
  -    let is_div = is_binop div_tm 
  -    let is_mod = is_binop mod_tm in
  -    fun tm -> is_div tm || is_mod tm
  -  let contains_quantifier =
  -    /// Tests for failure.
  -    let can f x = 
  -        try f x |> ignore; true
  -        with Failure _ -> false
  -    
  -    can (Choice.get << find_term (fun t -> is_forall t || is_exists t || is_uexists t))
  -  let BETA2_CONV = RATOR_CONV BETA_CONV |>THENC<| BETA_CONV
  -  let PRE_ELIM_THM'' = CONV_RULE (RAND_CONV NNF_CONV) PRE_ELIM_THM
  -  let SUB_ELIM_THM'' = CONV_RULE (RAND_CONV NNF_CONV) SUB_ELIM_THM
  -  let DIVMOD_ELIM_THM'' = CONV_RULE (RAND_CONV NNF_CONV) DIVMOD_ELIM_THM
  -  let pth_evenodd = 
  -    prove ((parse_term @"(EVEN(x) <=> (!y. ~(x = SUC(2 * y)))) /\
  +let NUM_SIMPLIFY_CONV = 
  +    let pre_tm = (parse_term @"PRE")
  +    let div_tm = (parse_term @"(DIV):num->num->num")
  +    let mod_tm = (parse_term @"(MOD):num->num->num")
  +    let p_tm = (parse_term @"P:num->bool")
  +    let n_tm = (parse_term @"n:num")
  +    let m_tm = (parse_term @"m:num")
  +    let q_tm = (parse_term @"P:num->num->bool")
  +    let a_tm = (parse_term @"a:num")
  +    let b_tm = (parse_term @"b:num")
  +    let is_pre tm = is_comb tm && Choice.get <| rator tm = pre_tm
  +    let is_sub = is_binop(parse_term @"(-):num->num->num")
  +    let is_divmod = 
  +        let is_div = is_binop div_tm
  +        let is_mod = is_binop mod_tm
  +        fun tm -> is_div tm || is_mod tm
  +    let contains_quantifier = 
  +        Choice.isResult << find_term(fun t -> is_forall t || is_exists t || is_uexists t)
  +    let BETA2_CONV = RATOR_CONV BETA_CONV
  +                     |> THENC <| BETA_CONV
  +    let PRE_ELIM_THM'' = CONV_RULE (RAND_CONV NNF_CONV) PRE_ELIM_THM
  +    let SUB_ELIM_THM'' = CONV_RULE (RAND_CONV NNF_CONV) SUB_ELIM_THM
  +    let DIVMOD_ELIM_THM'' = CONV_RULE (RAND_CONV NNF_CONV) DIVMOD_ELIM_THM
  +    let pth_evenodd = 
  +        prove((parse_term @"(EVEN(x) <=> (!y. ~(x = SUC(2 * y)))) /\
          (ODD(x) <=> (!y. ~(x = 2 * y))) /\
          (~EVEN(x) <=> (!y. ~(x = 2 * y))) /\
          (~ODD(x) <=> (!y. ~(x = SUC(2 * y))))"),
  -      REWRITE_TAC[GSYM NOT_EXISTS_THM; GSYM EVEN_EXISTS; GSYM ODD_EXISTS] |>THEN<|
  -      REWRITE_TAC[NOT_EVEN; NOT_ODD]) in
  -  let rec NUM_MULTIPLY_CONV pos tm =
  -    if is_forall tm || is_exists tm || is_uexists tm then
  -       BINDER_CONV (NUM_MULTIPLY_CONV pos) tm
  -    elif is_imp tm && contains_quantifier tm then
  -        COMB2_CONV (RAND_CONV(NUM_MULTIPLY_CONV(not pos))) (NUM_MULTIPLY_CONV pos) tm
  -    elif (is_conj tm || is_disj tm || is_iff tm) && contains_quantifier tm then
  -         BINOP_CONV (NUM_MULTIPLY_CONV pos) tm
  -    elif is_neg tm && not pos && contains_quantifier tm then
  -       RAND_CONV (NUM_MULTIPLY_CONV (not pos)) tm
  -    else
  -       try 
  -           let t = Choice.get <| find_term (fun t -> is_pre t && free_in t tm) tm in
  -           let ty = Choice.get <| type_of t in
  -           let v = genvar ty in
  -           let p = Choice.get <| mk_abs(v,Choice.get <| subst [v,t] tm) in
  -           let th0 = if pos then PRE_ELIM_THM'' else PRE_ELIM_THM' in
  -           let th1 = INST [p,p_tm; Choice.get <| rand t,n_tm] th0 in
  -           let th2 = CONV_RULE(COMB2_CONV (RAND_CONV BETA_CONV)
  -                      (BINDER_CONV(RAND_CONV BETA_CONV))) th1 in
  -           CONV_RULE(RAND_CONV (NUM_MULTIPLY_CONV pos)) th2
  -       with 
  -       | Failure _ -> 
  -       try
  -           let t = Choice.get <| find_term (fun t -> is_sub t && free_in t tm) tm in
  -           let ty = Choice.get <| type_of t in
  -           let v = genvar ty in
  -           let p = Choice.get <| mk_abs(v,Choice.get <| subst [v,t] tm) in
  -           let th0 = if pos then SUB_ELIM_THM'' else SUB_ELIM_THM' in
  -           let th1 = INST [p,p_tm; Choice.get <| lhand t,a_tm; Choice.get <| rand t,b_tm] th0 in
  -           let th2 = CONV_RULE(COMB2_CONV (RAND_CONV BETA_CONV) (BINDER_CONV(RAND_CONV BETA_CONV))) th1 in
  -           CONV_RULE(RAND_CONV (NUM_MULTIPLY_CONV pos)) th2
  -       with 
  -       | Failure _ -> 
  -       try
  -           let t = Choice.get <| find_term (fun t -> is_divmod t && free_in t tm) tm in
  -           let x = Choice.get <| lhand t 
  -           let y = Choice.get <| rand t in
  -           let dtm = Choice.get <| mk_comb(Choice.get <| mk_comb(div_tm,x),y)
  -           let mtm = Choice.get <| mk_comb(Choice.get <| mk_comb(mod_tm,x),y) in
  -           let vd = genvar(Choice.get <| type_of dtm)
  -           let vm = genvar(Choice.get <| type_of mtm) in
  -           let p = list_mk_abs([vd;vm],Choice.get <| subst[vd,dtm; vm,mtm] tm) in
  -           let th0 = if pos then DIVMOD_ELIM_THM'' else DIVMOD_ELIM_THM' in
  -           let th1 = INST [p,q_tm; x,m_tm; y,n_tm] th0 in
  -           let th2 = CONV_RULE (COMB2_CONV (RAND_CONV BETA2_CONV) (funpow 2 BINDER_CONV (RAND_CONV BETA2_CONV))) th1 in
  -           CONV_RULE(RAND_CONV (NUM_MULTIPLY_CONV pos)) th2
  -       with 
  -       | Failure _ -> REFL tm in
  -  NUM_REDUCE_CONV |>THENC<|
  -  CONDS_CELIM_CONV |>THENC<|
  -  NNF_CONV |>THENC<|
  -  NUM_MULTIPLY_CONV true |>THENC<|
  -  NUM_REDUCE_CONV |>THENC<|
  -  GEN_REWRITE_CONV ONCE_DEPTH_CONV [pth_evenodd];;
  +              REWRITE_TAC [GSYM NOT_EXISTS_THM;
  +                           GSYM EVEN_EXISTS;
  +                           GSYM ODD_EXISTS]
  +              |> THEN <| REWRITE_TAC [NOT_EVEN; NOT_ODD])
  +    let rec NUM_MULTIPLY_CONV pos tm = 
  +        if is_forall tm || is_exists tm || is_uexists tm then BINDER_CONV (NUM_MULTIPLY_CONV pos) tm
  +        elif is_imp tm && contains_quantifier tm then 
  +            COMB2_CONV (RAND_CONV(NUM_MULTIPLY_CONV(not pos))) (NUM_MULTIPLY_CONV pos) tm
  +        elif (is_conj tm || is_disj tm || is_iff tm) && contains_quantifier tm then 
  +            BINOP_CONV (NUM_MULTIPLY_CONV pos) tm
  +        elif is_neg tm && not pos && contains_quantifier tm then RAND_CONV (NUM_MULTIPLY_CONV(not pos)) tm
  +        else 
  +            try 
  +                let t = Choice.get <| find_term (fun t -> is_pre t && free_in t tm) tm
  +                let ty = Choice.get <| type_of t
  +                let v = genvar ty
  +                let p = Choice.get <| mk_abs(v, Choice.get <| subst [v, t] tm)
  +                let th0 = 
  +                    if pos then PRE_ELIM_THM''
  +                    else PRE_ELIM_THM'
  +                let th1 = 
  +                    INST [p, p_tm;
  +                          Choice.get <| rand t, n_tm] th0
  +                let th2 = CONV_RULE (COMB2_CONV (RAND_CONV BETA_CONV) (BINDER_CONV(RAND_CONV BETA_CONV))) th1
  +                CONV_RULE (RAND_CONV(NUM_MULTIPLY_CONV pos)) th2
  +            with
  +            | Failure _ -> 
  +                try 
  +                    let t = Choice.get <| find_term (fun t -> is_sub t && free_in t tm) tm
  +                    let ty = Choice.get <| type_of t
  +                    let v = genvar ty
  +                    let p = Choice.get <| mk_abs(v, Choice.get <| subst [v, t] tm)
  +                    let th0 = 
  +                        if pos then SUB_ELIM_THM''
  +                        else SUB_ELIM_THM'
  +                    let th1 = 
  +                        INST [p, p_tm;
  +                              Choice.get <| lhand t, a_tm;
  +                              Choice.get <| rand t, b_tm] th0
  +                    let th2 = CONV_RULE (COMB2_CONV (RAND_CONV BETA_CONV) (BINDER_CONV(RAND_CONV BETA_CONV))) th1
  +                    CONV_RULE (RAND_CONV(NUM_MULTIPLY_CONV pos)) th2
  +                with
  +                | Failure _ -> 
  +                    try 
  +                        let t = Choice.get <| find_term (fun t -> is_divmod t && free_in t tm) tm
  +                        let x = Choice.get <| lhand t
  +                        let y = Choice.get <| rand t
  +                        let dtm = Choice.get <| mk_comb(Choice.get <| mk_comb(div_tm, x), y)
  +                        let mtm = Choice.get <| mk_comb(Choice.get <| mk_comb(mod_tm, x), y)
  +                        let vd = genvar(Choice.get <| type_of dtm)
  +                        let vm = genvar(Choice.get <| type_of mtm)
  +                        let p = 
  +                            list_mk_abs([vd; vm], 
  +                                        Choice.get <| subst [vd, dtm;
  +                                                             vm, mtm] tm)
  +                        let th0 = 
  +                            if pos then DIVMOD_ELIM_THM''
  +                            else DIVMOD_ELIM_THM'
  +                        let th1 = 
  +                            INST [p, q_tm;
  +                                  x, m_tm;
  +                                  y, n_tm] th0
  +                        let th2 = 
  +                            CONV_RULE (COMB2_CONV (RAND_CONV BETA2_CONV) (funpow 2 BINDER_CONV (RAND_CONV BETA2_CONV))) 
  +                                th1
  +                        CONV_RULE (RAND_CONV(NUM_MULTIPLY_CONV pos)) th2
  +                    with
  +                    | Failure _ -> REFL tm
  +    NUM_REDUCE_CONV
  +    |> THENC <| CONDS_CELIM_CONV
  +    |> THENC <| NNF_CONV
  +    |> THENC <| NUM_MULTIPLY_CONV true
  +    |> THENC <| NUM_REDUCE_CONV
  +    |> THENC <| GEN_REWRITE_CONV ONCE_DEPTH_CONV [pth_evenodd]
   
   (* ----------------------------------------------------------------------- *)
   (* Natural number version of ring procedure with this normalization.       *)
   (* ----------------------------------------------------------------------- *)
   
   /// Ring decision procedure instantiated to natural numbers.
  -let NUM_RING =
  -  let NUM_INTEGRAL_LEMMA = 
  -    prove ((parse_term @"(w = x + d) /\ (y = z + e) ==> ((w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))"), DISCH_THEN(fun th -> REWRITE_TAC[th]) 
  -     |>THEN<| REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC] 
  -     |>THEN<| ONCE_REWRITE_TAC [AC ADD_AC (parse_term @"a + b + c + d + e = a + c + e + b + d")] 
  -     |>THEN<| REWRITE_TAC[EQ_ADD_LCANCEL; EQ_ADD_LCANCEL_0; MULT_EQ_0]) in
  -  let NUM_INTEGRAL = 
  -    prove ((parse_term @"(!x. 0 * x = 0) /\
  +let NUM_RING = 
  +    let NUM_INTEGRAL_LEMMA = 
  +        prove((parse_term @"(w = x + d) /\ (y = z + e) ==> ((w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))"), 
  +              DISCH_THEN(fun th -> REWRITE_TAC [th])
  +              |> THEN <| REWRITE_TAC [LEFT_ADD_DISTRIB;
  +                                      RIGHT_ADD_DISTRIB;
  +                                      GSYM ADD_ASSOC]
  +              |> THEN <| ONCE_REWRITE_TAC [AC ADD_AC (parse_term @"a + b + c + d + e = a + c + e + b + d")]
  +              |> THEN <| REWRITE_TAC [EQ_ADD_LCANCEL; EQ_ADD_LCANCEL_0; MULT_EQ_0])
  +
  +    let NUM_INTEGRAL = 
  +        prove((parse_term @"(!x. 0 * x = 0) /\
        (!x y z. (x + y = x + z) <=> (y = z)) /\
        (!w x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))"),
  -     REWRITE_TAC[MULT_CLAUSES; EQ_ADD_LCANCEL] |>THEN<|
  -     REPEAT GEN_TAC |>THEN<|
  -     DISJ_CASES_TAC (SPECL [(parse_term @"w:num"); (parse_term @"x:num")] LE_CASES) |>THEN<|
  -     DISJ_CASES_TAC (SPECL [(parse_term @"y:num"); (parse_term @"z:num")] LE_CASES) |>THEN<|
  -     REPEAT(FIRST_X_ASSUM (CHOOSE_THEN SUBST1_TAC << REWRITE_RULE[LE_EXISTS])) |>THEN<|
  -     ASM_MESON_TAC[NUM_INTEGRAL_LEMMA; ADD_SYM; MULT_SYM]) in
  -  let rawring =
  -    RING(Choice.get << dest_numeral, Choice.get << mk_numeral, NUM_EQ_CONV,
  -         genvar bool_ty,(parse_term @"(+):num->num->num"),genvar bool_ty,
  -         genvar bool_ty,(parse_term @"(*):num->num->num"),genvar bool_ty,
  -         (parse_term @"(EXP):num->num->num"),
  -         NUM_INTEGRAL,TRUTH,NUM_NORMALIZE_CONV) in
  -  let initconv = NUM_SIMPLIFY_CONV |>THENC<| GEN_REWRITE_CONV DEPTH_CONV [ADD1]
  -  let t_tm = (parse_term @"T") in
  -  fun tm -> let th = initconv tm in
  -            if Choice.get <| rand(concl <| Choice.get th) = t_tm then th
  -            else EQ_MP (SYM th) (rawring(Choice.get <| rand(concl <| Choice.get th)));;
  +              REWRITE_TAC [MULT_CLAUSES; EQ_ADD_LCANCEL]
  +              |> THEN <| REPEAT GEN_TAC
  +              |> THEN <| DISJ_CASES_TAC(SPECL [(parse_term @"w:num");
  +                                               (parse_term @"x:num")] LE_CASES)
  +              |> THEN <| DISJ_CASES_TAC(SPECL [(parse_term @"y:num");
  +                                               (parse_term @"z:num")] LE_CASES)
  +              |> THEN <| REPEAT(FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC << REWRITE_RULE [LE_EXISTS]))
  +              |> THEN <| ASM_MESON_TAC [NUM_INTEGRAL_LEMMA; ADD_SYM; MULT_SYM])
  +
  +    let rawring = 
  +        RING
  +            (Choice.get << dest_numeral, Choice.get << mk_numeral, NUM_EQ_CONV, genvar bool_ty, 
  +             (parse_term @"(+):num->num->num"), genvar bool_ty, genvar bool_ty, (parse_term @"(*):num->num->num"), 
  +             genvar bool_ty, (parse_term @"(EXP):num->num->num"), NUM_INTEGRAL, TRUTH, NUM_NORMALIZE_CONV)
  +    let initconv = NUM_SIMPLIFY_CONV
  +                   |> THENC <| GEN_REWRITE_CONV DEPTH_CONV [ADD1]
  +
  +    let t_tm = (parse_term @"T")
  +    fun tm -> 
  +        let th = initconv tm
  +        if Choice.get <| rand(concl <| Choice.get th) = t_tm then th
  +        else EQ_MP (SYM th) (rawring(Choice.get <| rand(concl <| Choice.get th)))
  
positive.code:   (* Grobner basis algorithm.                                                *)
    (* ----------------------------------------------------------------------- *)
    
    let rec grobner_basis basis pairs =
      Format.print_string(string(length basis)+" basis elements and "+
                          string(length pairs)+" critical pairs");
      Format.print_newline();
      match pairs with
        [] -> basis
      | (l,(p1,p2))::opairs ->
            let (sp,hist as sph) = monic (reduce basis (spoly l p1 p2))
            if sp = [] || criterion2 basis (l,(p1,p2)) opairs
            then grobner_basis basis opairs else
            if constant_poly sp then grobner_basis (sph::basis) [] else
            let rawcps =
              map (fun p -> mlcm (hd(fst p)) (hd sp),align(p,sph)) basis
            let newcps = filter (fun (l,(p,q)) -> not(orthogonal l (fst p) (fst q))) rawcps
            grobner_basis (sph::basis)
                    (merge forder opairs (mergesort forder newcps))
    
    (* ----------------------------------------------------------------------- *)
    (* Interreduce initial polynomials.                                        *)
    (* ----------------------------------------------------------------------- *)
    
    let rec grobner_interreduce rpols ipols =
      match ipols with
        [] -> map monic (rev rpols)
      | p::ps -> let p' = reduce (rpols @ ps) p
                 if fst p' = [] then grobner_interreduce rpols ps
                 else grobner_interreduce (p'::rpols) ps
    
    (* ----------------------------------------------------------------------- *)
    (* Overall function.                                                       *)
    (* ----------------------------------------------------------------------- *)
    
    let grobner pols =
      let npols = map2 (fun p n -> p,Start n) pols (0--(length pols - 1))
      let phists = filter (fun (p,_) -> p <> []) npols
      let bas = grobner_interreduce [] (map monic phists)
      let prs0 = allpairs (fun x y -> x,y) bas bas
      let prs1 = filter (fun ((x,_),(y,_)) -> poly_lt x y) prs0
      let prs2 = map (fun (p,q) -> mlcm (hd(fst p)) (hd(fst q)),(p,q)) prs1
      let prs3 =
        filter (fun (l,(p,q)) -> not(orthogonal l (fst p) (fst q))) prs2
      grobner_basis bas (mergesort forder prs3)
    
    (* ----------------------------------------------------------------------- *)
    (* Get proof of contradiction from Grobner basis.                          *)
    (* ----------------------------------------------------------------------- *)
    
    let grobner_refute pols =
      let gb = grobner pols
      snd(Option.get <| find (fun (p,h) -> length p = 1 && forall ((=)0) (snd(hd p))) gb)
    
    (* ----------------------------------------------------------------------- *)
    (* Turn proof into a certificate as sum of multipliers.                    *)
  
negative.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
            (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.  *)
  