let rec DISJ_TAC thm = DISJ_CASES_TAC thm THENL[ALL_TAC;TRY (POP_ASSUM DISJ_TAC)];;
let INTERPSIGNS_CONJ = prove_by_refinement(
  `!P Q eqs l.
    interpsigns eqs (\x. P x) l /\
    interpsigns eqs (\x. Q x) l ==>
    interpsigns eqs (\x. P x \/ Q x) l`,
(* {{{ Proof *)
[
  STRIP_TAC THEN STRIP_TAC;
  REPEAT LIST_INDUCT_TAC THEN REWRITE_TAC[interpsigns;
ALL2;interpsign];
  REPEAT (POP_ASSUM MP_TAC);
  DISJ_TAC (ISPEC `h':sign` 
SIGN_CASES) THEN ASM_REWRITE_TAC[interpsign;interpsigns] THEN REPEAT STRIP_TAC THEN ASM_MESON_TAC[];
]);;
 
let SUBLIST_MATCH = prove_by_refinement(
  `!h t l. 
SUBLIST (CONS h t) l ==>
     ?(l1:A list) l2. (l = 
APPEND l1 (CONS h l2)) /\ 
SUBLIST t l2`,
(* {{{ Proof *)
[
  STRIP_TAC;
  REPEAT LIST_INDUCT_TAC;
  REWRITE_TAC[
SUBLIST;
NOT_CONS_NIL;];
  CASES_ON `h = h'`;
  POP_ASSUM (REWRITE_ALL o list);
  STRIP_TAC;
  EXISTS_TAC `[]`;
  REWRITE_TAC[
APPEND;
SUBLIST_NIL];
  ASM_MESON_TAC[];
  REWRITE_TAC[
SUBLIST_NIL];
  STRIP_TAC;
  CLAIM `
SUBLIST [h] t`;
  ASM_MESON_TAC[
SUBLIST_NEQ];
  DISCH_THEN (REWRITE_ASSUMS o list);
  REPEAT (POP_ASSUM MP_TAC);
  REPEAT STRIP_TAC;
  EXISTS_TAC `CONS h' l1`;
  EXISTS_TAC `l2`;
  REWRITE_TAC[
APPEND];
  AP_TERM_TAC;
  ASM_MESON_TAC[];
  REWRITE_TAC[
SUBLIST;
NOT_CONS_NIL;];
  (* save *)
  CASES_ON `h = h''`;
  POP_ASSUM (REWRITE_ALL o list);
  STRIP_TAC;
  REWRITE_ASSUMS[
SUBLIST_CONS_CONS];
  EXISTS_TAC `[]:A list`;
  EXISTS_TAC `t'`;
  ASM_MESON_TAC[
APPEND];
  (* save *)
  STRIP_TAC;
  CLAIM `
SUBLIST (CONS h (CONS h' t)) t'`;
  ASM_MESON_TAC[
SUBLIST_NEQ];
  DISCH_THEN (REWRITE_ASSUMS o list);
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  EXISTS_TAC `CONS h'' l1`;
  EXISTS_TAC `l2`;
  ASM_REWRITE_TAC[
APPEND];
]);;
 
let n_nz = prove(mk_neg(mk_eq(n_tm,zero)),ARITH_TAC) in
      let not_nil_thm = EQ_MP (REWRITE_RULE[len_thm] (AP_TERM neg (ISPEC t LENGTH_0))) n_nz in
      let n_suc = prove(mk_eq(n_tm,mk_comb(`SUC`,pren_tm)),ARITH_TAC) in
      let len_tl = REWRITE_RULE[n_suc;PRE;ISPEC (mk_comb(tl_tm,t)) pre_thm;len_thm] (MATCH_MP LENGTH_TL not_nil_thm) in
      let cons_thm = MATCH_MP (ISPEC t HD_TL) not_nil_thm in
      let hd_thm = ONCE_REWRITE_RULE[HD_LEM] len_tl in
      let thm = REWRITE_RULE[GSYM cons_thm] hd_thm in
      let x0 = mk_var("x" ^ string_of_int n,ty) in
      let hdt = mk_comb(hd_tm,t) in
      let ex_thm = EXISTS (mk_exists(x0,subst[x0,hdt] (concl thm)),mk_comb(hd_tm,t)) thm in
      let left = DISCH (concl len_thm) ex_thm in
      let right = prove(mk_imp(concl ex_thm,concl len_thm),REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC) in
        GEN_ALL(MATCH_MPL[imp_thm;left;right]);;let INFERISIGN_POS_POS_POS = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Unknown (CONS Pos r2))
            (CONS (CONS Pos r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Pos (CONS Pos r2))
            (CONS (CONS Pos r3) rgns))))`,
 
let INFERISIGN_POS_POS_NEG = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Unknown (CONS Neg r2))
            (CONS (CONS Pos r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Pos (CONS Neg r2))
            (CONS (CONS Pos r3) rgns))))`,
 
let INFERISIGN_NEG_NEG_POS = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Unknown (CONS Pos r2))
            (CONS (CONS Neg r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Neg (CONS Pos r2))
            (CONS (CONS Neg r3) rgns))))`,
 
let INFERISIGN_NEG_NEG_NEG = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Unknown (CONS Neg r2))
            (CONS (CONS Neg r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Neg (CONS Neg r2))
            (CONS (CONS Neg r3) rgns))))`,
 
let INFERISIGN_POS_NEG_POS = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Unknown (CONS Pos r2))
            (CONS (CONS Neg r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    ?w. interpmat (
APPEND pts (CONS y (CONS w (CONS z qts))))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
          (CONS (CONS Pos (CONS Pos r2))
          (CONS (CONS Zero (CONS Pos r2))
          (CONS (CONS Neg (CONS Pos r2))
          (CONS (CONS Neg r3) rgns))))))`,
 
let INFERISIGN_POS_NEG_NEG = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Unknown (CONS Neg r2))
            (CONS (CONS Neg r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    ?w. interpmat (
APPEND pts (CONS y (CONS w (CONS z qts))))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
          (CONS (CONS Pos (CONS Neg r2))
          (CONS (CONS Zero (CONS Neg r2))
          (CONS (CONS Neg (CONS Neg r2))
          (CONS (CONS Neg r3) rgns))))))`,
 
let INFERISIGN_NEG_POS_NEG = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Unknown (CONS Neg r2))
            (CONS (CONS Pos r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    ?w. interpmat (
APPEND pts (CONS y (CONS w (CONS z qts))))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
          (CONS (CONS Neg (CONS Neg r2))
          (CONS (CONS Zero (CONS Neg r2))
          (CONS (CONS Pos (CONS Neg r2))
          (CONS (CONS Pos r3) rgns))))))`,
 
let INFERISIGN_NEG_POS_POS = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Unknown (CONS Pos r2))
            (CONS (CONS Pos r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    ?w. interpmat (
APPEND pts (CONS y (CONS w (CONS z qts))))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
          (CONS (CONS Neg (CONS Pos r2))
          (CONS (CONS Zero (CONS Pos r2))
          (CONS (CONS Pos (CONS Pos r2))
          (CONS (CONS Pos r3) rgns))))))`,
 
let INFERISIGN_ZERO_POS_POS = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Zero r1)
           (CONS (CONS Unknown (CONS Pos r2))
            (CONS (CONS Pos r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Zero r1)
           (CONS (CONS Pos (CONS Pos r2))
            (CONS (CONS Pos r3) rgns))))`,
 
let INFERISIGN_ZERO_POS_NEG = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Zero r1)
           (CONS (CONS Unknown (CONS Neg r2))
            (CONS (CONS Pos r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Zero r1)
           (CONS (CONS Pos (CONS Neg r2))
            (CONS (CONS Pos r3) rgns))))`,
 
let INFERISIGN_POS_ZERO_POS = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Unknown (CONS Pos r2))
            (CONS (CONS Zero r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Pos (CONS Pos r2))
            (CONS (CONS Zero r3) rgns))))`,
 
let INFERISIGN_POS_ZERO_NEG = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Unknown (CONS Neg r2))
            (CONS (CONS Zero r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Pos r1)
           (CONS (CONS Pos (CONS Neg r2))
            (CONS (CONS Zero r3) rgns))))`,
 
let INFERISIGN_ZERO_NEG_POS = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Zero r1)
           (CONS (CONS Unknown (CONS Pos r2))
            (CONS (CONS Neg r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Zero r1)
           (CONS (CONS Neg (CONS Pos r2))
            (CONS (CONS Neg r3) rgns))))`,
 
let INFERISIGN_ZERO_NEG_NEG = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Zero r1)
           (CONS (CONS Unknown (CONS Neg r2))
            (CONS (CONS Neg r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Zero r1)
           (CONS (CONS Neg (CONS Neg r2))
            (CONS (CONS Neg r3) rgns))))`,
 
let INFERISIGN_NEG_ZERO_NEG = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Unknown (CONS Neg r2))
            (CONS (CONS Zero r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Neg (CONS Neg r2))
            (CONS (CONS Zero r3) rgns))))`,
 
let INFERISIGN_NEG_ZERO_POS = prove_by_refinement(
  `!y z p pts qts eqs sgns rgns r1 r2 r3.
     interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Unknown (CONS Pos r2))
            (CONS (CONS Zero r3) rgns)))) ==>
     (
LENGTH sgns = 2 * 
LENGTH pts + 1) ==>
    interpmat (
APPEND pts (CONS y (CONS z qts)))
      (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
        (
APPEND sgns
          (CONS (CONS Neg r1)
           (CONS (CONS Neg (CONS Pos r2))
            (CONS (CONS Zero r3) rgns))))`,
 
let INFIN_HD_POS_LEM = prove_by_refinement(
  `!pts p ps r1 sgns.
  interpmat pts
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (CONS (CONS Unknown (CONS Pos r1)) sgns)  ==>
   nonconstant p ==>
  ?xminf.
   interpmat (CONS xminf pts)
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
      (CONS (CONS Neg (CONS Pos r1))
      (CONS (CONS Neg (CONS Pos r1))
      (CONS (CONS Unknown (CONS Pos r1)) sgns)))`,
 
let INFIN_TL_POS_LEM = prove_by_refinement(
  `!pts p ps r1 sgns r2.
  interpmat pts
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND sgns [a; b; CONS Unknown (CONS Pos r2)]) ==>
   nonconstant p ==>
  ?xinf.
   interpmat (
APPEND pts [xinf])
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND sgns
     [a; b; CONS Unknown (CONS Pos r2);
      CONS Pos (CONS Pos r2);
      CONS Pos (CONS Pos r2)])`,
 
let INFIN_HD_NEG_LEM = prove_by_refinement(
  `!pts p ps r1 sgns.
  interpmat pts
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (CONS (CONS Unknown (CONS Neg r1)) sgns)  ==>
   nonconstant p ==>
  ?xminf.
   interpmat (CONS xminf pts)
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
      (CONS (CONS Pos (CONS Neg r1))
      (CONS (CONS Pos (CONS Neg r1))
      (CONS (CONS Unknown (CONS Neg r1)) sgns)))`,
 
let INFIN_TL_NEG_LEM = prove_by_refinement(
  `!pts p ps r1 sgns r2.
  interpmat pts
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND sgns [a; b; CONS Unknown (CONS Neg r2)]) ==>
   nonconstant p ==>
  ?xinf.
   interpmat (
APPEND pts [xinf])
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND sgns
     [a; b; CONS Unknown (CONS Neg r2);
      CONS Neg (CONS Neg r2);
      CONS Neg (CONS Neg r2)])`,
 
let INFIN_POS_POS = prove_by_refinement(
  `!pts p ps r1 sgns r2.
  interpmat pts
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND (CONS (CONS Unknown (CONS Pos r1)) sgns)
     [a; b; CONS Unknown (CONS Pos r2)]) ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat (
APPEND (CONS xminf pts) [xinf])
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND
      (CONS (CONS Neg (CONS Pos r1))
      (CONS (CONS Neg (CONS Pos r1))
      (CONS (CONS Unknown (CONS Pos r1)) sgns)))
     [a; b; CONS Unknown (CONS Pos r2);
      CONS Pos (CONS Pos r2);
      CONS Pos (CONS Pos r2)])`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  REWRITE_ASSUMS[
APPEND];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_HD_POS_LEM);
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  EXISTS_TAC `xminf`;
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFIN_TL_POS_LEM);
  ASM_REWRITE_TAC[
APPEND;];
]);;
 
let INFIN_POS_NEG = prove_by_refinement(
  `!pts p ps r1 sgns r2.
  interpmat pts
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND (CONS (CONS Unknown (CONS Pos r1)) sgns)
     [a; b; CONS Unknown (CONS Neg r2)]) ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat (
APPEND (CONS xminf pts) [xinf])
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND
      (CONS (CONS Neg (CONS Pos r1))
      (CONS (CONS Neg (CONS Pos r1))
      (CONS (CONS Unknown (CONS Pos r1)) sgns)))
     [a; b; CONS Unknown (CONS Neg r2);
      CONS Neg (CONS Neg r2);
      CONS Neg (CONS Neg r2)])`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  REWRITE_ASSUMS[
APPEND];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_HD_POS_LEM);
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  EXISTS_TAC `xminf`;
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFIN_TL_NEG_LEM);
  ASM_REWRITE_TAC[
APPEND;];
]);;
 
let INFIN_NEG_POS = prove_by_refinement(
  `!pts p ps r1 sgns r2.
  interpmat pts
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND (CONS (CONS Unknown (CONS Neg r1)) sgns)
     [a; b; CONS Unknown (CONS Pos r2)]) ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat (
APPEND (CONS xminf pts) [xinf])
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND
      (CONS (CONS Pos (CONS Neg r1))
      (CONS (CONS Pos (CONS Neg r1))
      (CONS (CONS Unknown (CONS Neg r1)) sgns)))
     [a; b; CONS Unknown (CONS Pos r2);
      CONS Pos (CONS Pos r2);
      CONS Pos (CONS Pos r2)])`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  REWRITE_ASSUMS[
APPEND];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_HD_NEG_LEM);
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  EXISTS_TAC `xminf`;
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFIN_TL_POS_LEM);
  ASM_REWRITE_TAC[
APPEND;];
]);;
 
let INFIN_NEG_NEG = prove_by_refinement(
  `!pts p ps r1 sgns r2.
  interpmat pts
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND (CONS (CONS Unknown (CONS Neg r1)) sgns)
     [a; b; CONS Unknown (CONS Neg r2)]) ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat (
APPEND (CONS xminf pts) [xinf])
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    (
APPEND
      (CONS (CONS Pos (CONS Neg r1))
      (CONS (CONS Pos (CONS Neg r1))
      (CONS (CONS Unknown (CONS Neg r1)) sgns)))
     [a; b; CONS Unknown (CONS Neg r2);
      CONS Neg (CONS Neg r2);
      CONS Neg (CONS Neg r2)])`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  REWRITE_ASSUMS[
APPEND];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_HD_NEG_LEM);
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  EXISTS_TAC `xminf`;
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFIN_TL_NEG_LEM);
  ASM_REWRITE_TAC[
APPEND;];
]);;
 
let INFIN_NIL_POS = prove_by_refinement(
  `!p ps r1.
  interpmat []
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    [CONS Unknown (CONS Pos r1)]  ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat [xminf; xinf]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
      [CONS Neg (CONS Pos r1);
       CONS Neg (CONS Pos r1);
       CONS Unknown (CONS Pos r1);
       CONS Pos (CONS Pos r1);
       CONS Pos (CONS Pos r1)]`,
 
let INFIN_NIL_NEG = prove_by_refinement(
  `!p ps r1.
  interpmat []
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    [CONS Unknown (CONS Neg r1)]  ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat [xminf; xinf]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
      [CONS Pos (CONS Neg r1);
       CONS Pos (CONS Neg r1);
       CONS Unknown (CONS Neg r1);
       CONS Neg (CONS Neg r1);
       CONS Neg (CONS Neg r1)]`,
 
let INFIN_SING_POS_POS = prove_by_refinement(
  `!p ps r1 x s2 r2 r3.
  interpmat [x]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    [CONS Unknown (CONS Pos r1);CONS s2 r2;CONS Unknown (CONS Pos r3)]  ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat [xminf; x; xinf]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
      [CONS Neg (CONS Pos r1);
       CONS Neg (CONS Pos r1);
       CONS Unknown (CONS Pos r1);
       CONS s2 r2;
       CONS Unknown (CONS Pos r3);
       CONS Pos (CONS Pos r3);
       CONS Pos (CONS Pos r3)]`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  ONCE_REWRITE_ASSUMS[
prove(`[x; y; z] = 
APPEND [] [x; y; z]`,REWRITE_TAC[
APPEND])];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_TL_POS_LEM);
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  MATCH_MP_TAC (
prove(`(?y x. P x y) ==> (?x y. P x y)`,MESON_TAC[]));
  EXISTS_TAC `xinf`;
  REWRITE_ALL[
APPEND];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_HD_POS_LEM);
  ASM_REWRITE_TAC[];
]);;
 
let INFIN_SING_POS_NEG = prove_by_refinement(
  `!p ps r1 x s2 r2 r3.
  interpmat [x]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    [CONS Unknown (CONS Pos r1);CONS s2 r2;CONS Unknown (CONS Neg r3)]  ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat [xminf; x; xinf]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
      [CONS Neg (CONS Pos r1);
       CONS Neg (CONS Pos r1);
       CONS Unknown (CONS Pos r1);
       CONS s2 r2;
       CONS Unknown (CONS Neg r3);
       CONS Neg (CONS Neg r3);
       CONS Neg (CONS Neg r3)]`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  ONCE_REWRITE_ASSUMS[
prove(`[x; y; z] = 
APPEND [] [x; y; z]`,REWRITE_TAC[
APPEND])];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_TL_NEG_LEM);
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  MATCH_MP_TAC (
prove(`(?y x. P x y) ==> (?x y. P x y)`,MESON_TAC[]));
  EXISTS_TAC `xinf`;
  REWRITE_ALL[
APPEND];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_HD_POS_LEM);
  ASM_REWRITE_TAC[];
]);;
 
let INFIN_SING_NEG_POS = prove_by_refinement(
  `!p ps r1 x s2 r2 r3.
  interpmat [x]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    [CONS Unknown (CONS Neg r1);CONS s2 r2;CONS Unknown (CONS Pos r3)]  ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat [xminf; x; xinf]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
      [CONS Pos (CONS Neg r1);
       CONS Pos (CONS Neg r1);
       CONS Unknown (CONS Neg r1);
       CONS s2 r2;
       CONS Unknown (CONS Pos r3);
       CONS Pos (CONS Pos r3);
       CONS Pos (CONS Pos r3)]`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  ONCE_REWRITE_ASSUMS[
prove(`[x; y; z] = 
APPEND [] [x; y; z]`,REWRITE_TAC[
APPEND])];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_TL_POS_LEM);
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  MATCH_MP_TAC (
prove(`(?y x. P x y) ==> (?x y. P x y)`,MESON_TAC[]));
  EXISTS_TAC `xinf`;
  REWRITE_ALL[
APPEND];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_HD_NEG_LEM);
  ASM_REWRITE_TAC[];
]);;
 
let INFIN_SING_NEG_NEG = prove_by_refinement(
  `!p ps r1 x s2 r2 r3.
  interpmat [x]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
    [CONS Unknown (CONS Neg r1);CONS s2 r2;CONS Unknown (CONS Neg r3)]  ==>
   nonconstant p ==>
  ?xminf xinf.
   interpmat [xminf; x; xinf]
    (CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
      [CONS Pos (CONS Neg r1);
       CONS Pos (CONS Neg r1);
       CONS Unknown (CONS Neg r1);
       CONS s2 r2;
       CONS Unknown (CONS Neg r3);
       CONS Neg (CONS Neg r3);
       CONS Neg (CONS Neg r3)]`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  ONCE_REWRITE_ASSUMS[
prove(`[x; y; z] = 
APPEND [] [x; y; z]`,REWRITE_TAC[
APPEND])];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_TL_NEG_LEM);
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  MATCH_MP_TAC (
prove(`(?y x. P x y) ==> (?x y. P x y)`,MESON_TAC[]));
  EXISTS_TAC `xinf`;
  REWRITE_ALL[
APPEND];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
INFIN_HD_NEG_LEM);
  ASM_REWRITE_TAC[];
]);;
 
let ALL2_EL_LT_LEM = prove_by_refinement(
  `!k P l1 l2 n.
    (k = 
LENGTH l1) /\ 
ALL2 P l1 l2 /\ n < k ==>
       P (
EL n l1) (
EL n l2)`,
(* {{{ Proof *)
[
  INDUCT_TAC;
  REPEAT STRIP_TAC;
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REPEAT STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_LENGTH);
  STRIP_TAC;
  CLAIM `~(l1 = [])`;
  REWRITE_TAC[GSYM 
LENGTH_0];
  REPEAT_N 3 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL;];
  STRIP_TAC;
  CLAIM `~(l2 = [])`;
  REWRITE_TAC[GSYM 
LENGTH_0];
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (SUBST1_TAC o GSYM);
  REPEAT_N 2 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL;];
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ASSUMS[
LENGTH;
SUC_INJ;
ALL2;];
  REPEAT_N 3 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  (* save *)
  DISJ_CASES_TAC (ISPEC `n:num` 
num_CASES);
  POP_ASSUM (REWRITE_ALL o list);
  ASM_REWRITE_TAC[
EL;
HD];
  POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
TL;];
  REWRITE_ASSUMS[
LENGTH;
SUC_INJ;
ALL2;
LT_SUC];
  FIRST_ASSUM MATCH_MP_TAC;
  ASM_REWRITE_TAC[];
]);;
 
let ALL2_EL_LEM = prove_by_refinement(
  `!k P (l1:A list) (l2:B list).  (k = 
LENGTH l1) /\ (k = 
LENGTH l2) /\
    ~(?i. i < 
LENGTH l1 /\ ~(P (
EL i l1) (
EL i l2))) ==> 
ALL2 P l1 l2`,
(* {{{ Proof *)
[
  INDUCT_TAC;
  REPEAT STRIP_TAC;
  EVERY_ASSUM (MP_TAC o GSYM);
  ASM_MESON_TAC[
LENGTH_0;
ALL2];
  REPEAT STRIP_TAC;
  CLAIM `~(l1 = [])`;
  REWRITE_TAC[GSYM 
LENGTH_0];
  REPEAT_N 2 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL;];
  STRIP_TAC;
  CLAIM `~(l2 = [])`;
  REWRITE_TAC[GSYM 
LENGTH_0];
  REPEAT_N 2 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL;];
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
LENGTH;
SUC_INJ;
ALL2;];
  STRIP_TAC;
  ASM_MESON_TAC[
LT_0;
EL;
HD;];
  (* save *)
  FIRST_ASSUM MATCH_MP_TAC;
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  ASM_MESON_TAC[];
  REPEAT STRIP_TAC;
  CLAIM `SUC i < SUC (
LENGTH t)`;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  REPEAT_N 3 (POP_ASSUM MP_TAC);
  REWRITE_ASSUMS[
NOT_EXISTS_THM];
  POP_ASSUM (ASSUME_TAC o ISPEC `SUC i`);
  REWRITE_ALL[
LT_SUC];
  REWRITE_ALL[
EL;
TL;];
  ASM_MESON_TAC[];
]);;
 
let REMOVE_HD_COL = prove_by_refinement(
  `!p ps sgns pts.
    interpmat pts (CONS p ps) sgns ==> interpmat pts ps (
MAP TL sgns)`,
(* {{{ Proof *)
[
  REWRITE_TAC[interpmat;
ALL2_EL];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[
ALL2_EL];
  ASM_MESON_TAC[
LENGTH_MAP];
  REWRITE_ASSUMS[
NOT_EXISTS_THM];
  REPEAT_N 2 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `i:num`);
  REWRITE_TAC[DE_MORGAN_THM];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[];
  REWRITE_ALL[interpsigns];
  CLAIM `i < 
LENGTH sgns`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  ASM_SIMP_TAC[
EL_MAP];
  REWRITE_ALL[interpsigns];
  CLAIM `~(
EL i sgns = [])`;
  REWRITE_TAC[GSYM 
LENGTH_0];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_LENGTH);
  REWRITE_TAC[
LENGTH];
  ARITH_TAC;
  (* save *)
  DISCH_THEN (MP_TAC o MATCH_MP 
HD_TL);
  DISCH_THEN (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN SUBST1_TAC x);
  REWRITE_TAC[
ALL2;
TL;];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
]);;
 
let REMOVE_COL1 = prove_by_refinement(
  `!sgns pts p1 p2 ps.
   interpmat pts (CONS p1 (CONS p2 ps)) sgns ==>
   interpmat pts (CONS p1 ps) (
MAP (\x. CONS (
HD x) (
TL (
TL x))) sgns)`,
(* {{{ Proof *)
[
  REWRITE_TAC[interpmat;
ALL2_EL];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[
LENGTH_MAP];
  REWRITE_ASSUMS[
NOT_EXISTS_THM];
  REPEAT_N 2 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `i:num`);
  REWRITE_TAC[DE_MORGAN_THM];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[];
  REWRITE_ALL[interpsigns];
  CLAIM `i < 
LENGTH sgns`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  ASM_SIMP_TAC[
EL_MAP];
  REWRITE_ALL[interpsigns];
  CLAIM `~(
EL i sgns = [])`;
  REWRITE_TAC[GSYM 
LENGTH_0];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_LENGTH);
  REWRITE_TAC[
LENGTH];
  ARITH_TAC;
  (* save *)
  DISCH_THEN (MP_TAC o MATCH_MP 
HD_TL);
  DISCH_THEN (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN SUBST1_TAC x);
  REWRITE_TAC[
ALL2;
TL;];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[
HD;];
  CLAIM `~(
TL (
EL i sgns) = [])`;
  REWRITE_TAC[GSYM 
LENGTH_0];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_LENGTH);
  REWRITE_TAC[
LENGTH];
  ARITH_TAC;
  (* save *)
  DISCH_THEN (MP_TAC o MATCH_MP 
HD_TL);
  DISCH_THEN (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN SUBST1_TAC x);
  REWRITE_TAC[
ALL2;
TL;];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[
HD;];
]);;
 
let ALL_EL = prove_by_refinement(
  `!P l. 
ALL P l <=> !n. n < 
LENGTH l ==> P (
EL n l)`,
(* {{{ Proof *)
[
  STRIP_TAC;
  LIST_INDUCT_TAC;
  REWRITE_TAC[
ALL;
LENGTH];
  ARITH_TAC;
  ASM_REWRITE_TAC[
ALL];
  POP_ASSUM (fun x -> ALL_TAC);
  EQ_TAC;
  REPEAT STRIP_TAC;
  CASES_ON `n = 0`;
  POP_ASSUM (REWRITE_ALL o list);
  ASM_REWRITE_TAC[
EL;
HD;];
  REWRITE_ASSUMS[
LENGTH];
  CLAIM `
PRE n < 
LENGTH t`;
  POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
  DISCH_THEN (fun x -> FIRST_ASSUM (MP_TAC o C MATCH_MP x));
  ASM_MESON_TAC[
EL_PRE];
  (* save *)
  REPEAT STRIP_TAC;
  REWRITE_ASSUMS[
LENGTH];
  FIRST_ASSUM (MP_TAC o ISPEC `0`);
  REWRITE_TAC[
EL;
HD;];
  MESON_TAC[
LT_0];
  REWRITE_ASSUMS[
LENGTH];
  CLAIM `SUC n < SUC (
LENGTH t)`;
  ASM_MESON_TAC[
LT_SUC];
  DISCH_THEN (fun x -> FIRST_ASSUM (MP_TAC o C MATCH_MP x));
  REWRITE_TAC[
EL_SUC];
]);;
 
let REMOVE_LAST = prove_by_refinement(
  `!pts pols sgns .
     interpmat pts pols sgns ==>
     interpmat pts (
BUTLAST pols) (
MAP BUTLAST sgns)`,
(* {{{ Proof *)
[
  REWRITE_TAC[interpmat;
ALL2_EL];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[
LENGTH_MAP];
  REWRITE_ASSUMS[
NOT_EXISTS_THM];
  REPEAT_N 2 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `i:num`);
  REWRITE_TAC[DE_MORGAN_THM];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[];
  REWRITE_ALL[interpsigns];
  CLAIM `i < 
LENGTH sgns`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  (* save *)
  ASM_SIMP_TAC[
EL_MAP];
  ASM_MESON_TAC[
ALL2_BUTLAST];
]);;
 
let MAP2_EL_LEM = prove_by_refinement(
  `!f k l1 l2 i. (
LENGTH l1 = 
LENGTH l2) ==> i < 
LENGTH l1 ==>
    (k = 
LENGTH l1) ==>
     (
EL i (
MAP2 f l1 l2) = f (
EL i l1) (
EL i l2))`,
(* {{{ Proof *)
[
  STRIP_TAC;
  INDUCT_TAC;
  REPEAT STRIP_TAC;
  POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
  REPEAT STRIP_TAC;
  CLAIM `~(l1 = [])`;
  ASM_MESON_TAC[
LENGTH_0;
NOT_SUC];
  CLAIM `~(l2 = [])`;
  ASM_MESON_TAC[
LENGTH_0;
NOT_SUC];
  REWRITE_TAC[
NOT_NIL];
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
MAP2];
  REWRITE_ALL[
LENGTH;
SUC_INJ];
  DISJ_CASES_TAC (ISPEC `i:num` 
num_CASES);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
HD;];
  POP_ASSUM MP_TAC THEN STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
TL;];
  REWRITE_ASSUMS[
LT_SUC];
  ASM_MESON_TAC[];
]);;
 
let INSERTAT_EL = prove_by_refinement(
  `!n (x:A) i l. n <= 
LENGTH l ==> i <= 
LENGTH l ==>
   ((i < n ==> (
EL i (
INSERTAT n x l) = 
EL i l)) /\
   ((i = n) ==> (
EL i (
INSERTAT n x l) = x)) /\
   (i > n ==> (
EL i (
INSERTAT n x l) = 
EL (
PRE i) l)))`,
(* {{{ Proof *)
[
  INDUCT_TAC;
  REPEAT STRIP_TAC;
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  ASM_REWRITE_TAC[
INSERTAT;
EL;
HD;];
  ASM_REWRITE_TAC[
INSERTAT;
EL;
HD;];
  DISJ_CASES_TAC (ISPEC `i:num` 
num_CASES);
  EVERY_ASSUM MP_TAC THEN ARITH_TAC;
  POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
TL;
PRE];
  (* save *)
  REPEAT_N 5 STRIP_TAC;
  CLAIM `~(l = [])`;
  ASM_MESON_TAC[
LENGTH_0;
NOT_LE;ARITH_RULE `~(SUC n <= 0)`];
  STRIP_TAC;
  CLAIM `n <= 
LENGTH (
TL l)`;
  ASM_SIMP_TAC[
LENGTH_TL];
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  (* save *)
  REPEAT STRIP_TAC;
  REWRITE_TAC[
INSERTAT];
  NUM_CASES_TAC `i`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
HD;];
  POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
TL;];
  CLAIM `n' <= 
LENGTH (
TL l)`;
  REWRITE_ASSUMS[
LT_SUC];
  ASM_MESON_TAC[
LTE_TRANS;
LT_TRANS;
LET_TRANS;
LT_IMP_LE];
  STRIP_TAC;
  REWRITE_ASSUMS[
LT_SUC];
  ASM_MESON_TAC[];
  (* save *)
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
INSERTAT;
TL;];
  ASM_MESON_TAC[];
  REWRITE_TAC[
INSERTAT];
  NUM_CASES_TAC `i`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
HD;
PRE];
  (* save *)
  POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
TL;
PRE];
  CLAIM `n' <= 
LENGTH (
TL l)`;
  ASM_SIMP_TAC[
LENGTH_TL];
  REPEAT_N 3 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  REWRITE_ASSUMS[
GT;
LT_SUC];
  FIRST_X_ASSUM (MP_TAC o ISPECL[`x:A`;`n':num`;`
TL l:A list`]);
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  NUM_CASES_TAC `n'`;
  ASM_MESON_TAC[ARITH_RULE `x < y ==> ~(y = 0)`];
  POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
PRE;
EL];
]);;
 
let MATINSERT_THM = prove_by_refinement(
  `!pts p pols n psgns sgns.
     interpmat pts pols sgns ==>
     
ALL2 (\x y. interpsign x p y) (
partition_line pts) psgns ==>
     n <= 
LENGTH pols ==>
      interpmat pts (
INSERTAT n p pols) (
MAP2 (
INSERTAT n) psgns sgns)`,
(* {{{ Proof *)
[
  REWRITE_TAC[interpmat;
ALL2_EL;
NOT_EXISTS_THM;DE_MORGAN_THM;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  ASM_REWRITE_TAC[];
  CLAIM `
LENGTH (psgns:sign list) = 
LENGTH sgns`;
  ASM_MESON_TAC[
LENGTH_MAP2];
  ASM_MESON_TAC[
LENGTH_MAP2];
  DISJ_LCASE;
  REWRITE_ASSUMS[];
  (* save *)
  REWRITE_ALL[interpsigns];
  CLAIM `
LENGTH psgns = 
LENGTH sgns`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  CLAIM `i < 
LENGTH psgns`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  ASM_SIMP_TAC[
MAP2_EL];
  (* save *)
  REWRITE_TAC[
ALL2_EL];
  REWRITE_TAC[
NOT_EXISTS_THM;DE_MORGAN_THM];
  REPEAT STRIP_TAC;
  ASM_SIMP_TAC[
INSERTAT_LENGTH];
  CLAIM `
LENGTH (
EL i (sgns:(sign list) list)) = 
LENGTH pols`;
  ASM_MESON_TAC[
ALL2_LENGTH];
  STRIP_TAC;
  ASM_SIMP_TAC[
INSERTAT_LENGTH];
  (* save *)
  DISJ_LCASE;
  REWRITE_ASSUMS[];
  MP_TAC (ARITH_RULE `i' < n \/ (i' = n) \/ i' > (n:num)`);
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
EL i sgns) = 
LENGTH pols`;
  ASM_MESON_TAC[
ALL2_LENGTH];
  STRIP_TAC;
  CLAIM `n <= 
LENGTH (
EL i sgns)`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  CLAIM `i' <= 
LENGTH (
EL i sgns)`;
  ASM_MESON_TAC[
LTE_TRANS;
LET_TRANS;
LT_TRANS;
LT_IMP_LE];
  STRIP_TAC;
  ASM_SIMP_TAC[
INSERTAT_EL];
  CLAIM `i' <= 
LENGTH pols`;
  ASM_MESON_TAC[
LTE_TRANS;
LET_TRANS;
LT_TRANS;
LT_IMP_LE];
  STRIP_TAC;
  ASM_SIMP_TAC[
INSERTAT_EL];
  REPEAT_N 12 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `i:num`);
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[];
  LABEL_ALL_TAC;
  USE_THEN "Z-12" MP_TAC;
  REWRITE_TAC[
ALL2_EL];
  REWRITE_TAC[
NOT_EXISTS_THM;DE_MORGAN_THM];
  STRIP_TAC;
  POP_ASSUM (MP_TAC o ISPEC `i':num`);
  POP_ASSUM (fun x -> ALL_TAC);
  ASM_REWRITE_TAC[];
  POP_ASSUM (fun x -> ALL_TAC);
  STRIP_TAC;
  ASM_MESON_TAC[ARITH_RULE `x <= y /\ z < x ==> z < (y:num)`];
  (* save *)
  POP_ASSUM (REWRITE_ALL o list);
  CLAIM `
LENGTH (
EL i sgns) = 
LENGTH pols`;
  ASM_MESON_TAC[
ALL2_LENGTH];
  STRIP_TAC;
  CLAIM `n <= 
LENGTH (
EL i sgns)`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  ASM_SIMP_TAC[
INSERTAT_EL];
  ASM_MESON_TAC[
ALL2_EL];
  (* save *)
  CLAIM `
LENGTH (
EL i sgns) = 
LENGTH pols`;
  ASM_MESON_TAC[
ALL2_LENGTH];
  STRIP_TAC;
  CLAIM `n <= 
LENGTH (
EL i sgns)`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  CLAIM `i' <= 
LENGTH (
EL i sgns)`;
  ASM_REWRITE_TAC[];
  LABEL_ALL_TAC;
  USE_THEN "Z-7" (MP_TAC o MATCH_MP 
INSERTAT_LENGTH);
  TYPE_TAC (fun x -> DISCH_THEN (MP_TAC o ISPEC x)) `p`;
  USE_THEN "Z-3" MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  CLAIM `i' <= 
LENGTH pols`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  ASM_SIMP_TAC[
INSERTAT_EL];
  LABEL_ALL_TAC;
  (* save *)
  USE_X_ASSUM "Z-12" (MP_TAC o ISPEC `i:num`);
  ASM_REWRITE_TAC[];
  REWRITE_TAC[
ALL2_EL];
  ASM_REWRITE_TAC[
NOT_EXISTS_THM;DE_MORGAN_THM;];
  DISCH_THEN (MP_TAC o ISPEC `
PRE i':num`);
  STRIP_TAC;
  CLAIM `~(i' = 0)`;
  USE_THEN "Z-4" MP_TAC THEN ARITH_TAC;
  POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
]);;
 
let EL_REPLICATE = prove_by_refinement(
  `!n x i. i < n ==> (
EL i (
REPLICATE n x) = x)`,
(* {{{ Proof *)
[
  INDUCT_TAC;
  ARITH_TAC;
  REPEAT STRIP_TAC;
  REWRITE_TAC[
REPLICATE];
  NUM_CASES_TAC `i`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
HD;];
  POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  REWRITE_TAC[
EL;
TL;];
  ASM_MESON_TAC[
LT_SUC];
]);;
 
let INFERPSIGN_POS = prove_by_refinement(
  `!p ps q qs r rs s x pts1 pts2  s1 s2 s3 rest sgns.
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (
LENGTH sgns = 2 * 
LENGTH pts1 + 1) ==>
  (!x. p x = s x * q x + r x) ==>
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Pos s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
  REWRITE_TAC[interpmat];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
  CASES_ON `pts1 = []`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;];
  COND_CASES_TAC;
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 5 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
  FIRST_ASSUM MATCH_MP_TAC;
  REWRITE_TAC[];
  ASM_REWRITE_TAC[];
  (* save *)
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
  FIRST_ASSUM MATCH_MP_TAC;
  REWRITE_TAC[];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
  ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
  REPEAT STRIP_TAC;
  CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
     (CONS (\x'. 
LAST pts1 < x' /\ x' < x)
     (
TL (
partition_line (CONS x pts2))))) =
     (
APPEND
      (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x])
     (
TL (
partition_line (CONS x pts2))))`;
  ASM_MESON_TAC[
APPEND_CONS];
  DISCH_THEN (REWRITE_ALL o list);
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_ALL[
partition_line];
  COND_CASES_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  REWRITE_ALL[
TL;];
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  RESTRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
  FIRST_ASSUM MATCH_MP_TAC;
  REWRITE_TAC[];
  (* save *)
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
  FIRST_ASSUM MATCH_MP_TAC;
  REWRITE_TAC[];
]);;
 
let INFERPSIGN_NEG = prove_by_refinement(
  `!p ps q qs r rs s x pts1 pts2  s1 s2 s3 rest sgns.
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (
LENGTH sgns = 2 * 
LENGTH pts1 + 1) ==>
  (!x. p x = s x * q x + r x) ==>
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Neg s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
  REWRITE_TAC[interpmat];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
  CASES_ON `pts1 = []`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;];
  COND_CASES_TAC;
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 5 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
  FIRST_ASSUM MATCH_MP_TAC;
  REWRITE_TAC[];
  ASM_REWRITE_TAC[];
  (* save *)
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
  FIRST_ASSUM MATCH_MP_TAC;
  REWRITE_TAC[];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
  ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
  REPEAT STRIP_TAC;
  CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
     (CONS (\x'. 
LAST pts1 < x' /\ x' < x)
     (
TL (
partition_line (CONS x pts2))))) =
     (
APPEND
      (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x])
     (
TL (
partition_line (CONS x pts2))))`;
  ASM_MESON_TAC[
APPEND_CONS];
  DISCH_THEN (REWRITE_ALL o list);
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_ALL[
partition_line];
  COND_CASES_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  REWRITE_ALL[
TL;];
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  RESTRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
  FIRST_ASSUM MATCH_MP_TAC;
  REWRITE_TAC[];
  (* save *)
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
  FIRST_ASSUM MATCH_MP_TAC;
  REWRITE_TAC[];
]);;
 
let INFERPSIGN_POS_EVEN_LEM = prove_by_refinement(
  `!a n p ps q qs r rs s x pts1 pts2  s1 s2 s3 rest sgns.
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (
LENGTH sgns = 2 * 
LENGTH pts1 + 1) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a <> &0) ==>
  
EVEN n ==>
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Pos s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `a pow n > &0`;
  ASM_MESON_TAC[
EVEN_ODD_POW];
  STRIP_TAC;
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[interpmat];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
  CASES_ON `pts1 = []`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;];
  COND_CASES_TAC;
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x > &0`;
  ASM_MESON_TAC[];
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x > &0`;
  ASM_MESON_TAC[];
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
  ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
  REPEAT STRIP_TAC;
  CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
     (CONS (\x'. 
LAST pts1 < x' /\ x' < x)
     (
TL (
partition_line (CONS x pts2))))) =
     (
APPEND
      (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x])
     (
TL (
partition_line (CONS x pts2))))`;
  ASM_MESON_TAC[
APPEND_CONS];
  DISCH_THEN (REWRITE_ALL o list);
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_ALL[
partition_line];
  COND_CASES_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  REWRITE_ALL[
TL;];
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  RESTRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x > &0`;
  ASM_MESON_TAC[];
  REPEAT_N 15 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  (* save *)
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 10 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x > &0`;
  ASM_MESON_TAC[];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 17 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`];
]);;
 
let SPLIT_LIST_THM = prove_by_refinement(
  `!n (l:A list). n < 
LENGTH l ==>
    ?l1 l2. (l = 
APPEND l1 l2) /\ (
LENGTH l1 = n)`,
(* {{{ Proof *)
[
  INDUCT_TAC;
  REPEAT STRIP_TAC;
  EXISTS_TAC `[]:A list`;
  EXISTS_TAC `l`;
  REWRITE_TAC[
APPEND;
LENGTH];
  REPEAT STRIP_TAC;
  CLAIM `n < 
LENGTH l`;
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  DISCH_THEN (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)));
  STRIP_TAC;
  EXISTS_TAC `
APPEND l1 [
HD l2]`;
  EXISTS_TAC `
TL (l2:A list)`;
  CLAIM `~((l2:A list) = [])`;
  REWRITE_TAC[GSYM 
LENGTH_0];
  STRIP_TAC;
  POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC;
  POP_ASSUM (MP_TAC o AP_TERM `LENGTH:A list -> num`);
  REWRITE_TAC[
LENGTH_APPEND];
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL;];
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  ASM_REWRITE_TAC[
TL;
HD;
LENGTH_APPEND;
LENGTH;];
  STRIP_TAC;
  REWRITE_TAC[
APPEND_APPEND;
APPEND;];
  ARITH_TAC;
]);;
 
let DIV_EVEN = prove_by_refinement(
 `!x. 
EVEN x ==> (2 * x DIV 2 = x)`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  TYPE_TACL (fun l -> MP_TAC (ISPECL l 
DIVISION)) [`x`;`2`];
  ARITH_SIMP_TAC[];
  REWRITE_ASSUMS[
EVEN_MOD];
  ASM_REWRITE_TAC[];
  ARITH_SIMP_TAC[];
  STRIP_TAC;
  REWRITE_ASSUMS[ARITH_RULE `x + 0 = x`];
  ONCE_REWRITE_ASSUMS[ARITH_RULE `x * y = y * x:num`];
  ASM_MESON_TAC[];
]);;
 
let INFERPSIGN_POS_EVEN = prove_by_refinement(
  `!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a <> &0) ==>
  
EVEN n ==>
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Pos s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
APPEND sgns (CONS
    (
APPEND (CONS Unknown s1)
      (
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) =
        
LENGTH (
partition_line pts)`;
  REWRITE_ALL[interpmat];
  ASM_MESON_TAC[
ALL2_LENGTH];
  REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
  STRIP_TAC;
  TYPE_TACL (fun l -> MP_TAC (ISPECL l 
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
  STRIP_TAC;
  LABEL_ALL_TAC;
  PROVE_ASSUM_ANTECEDENT_TAC 0;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  ARITH_TAC;
  POP_ASSUM MP_TAC THEN STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `~(l2 = [])`;
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  REWRITE_ALL[
APPEND_NIL];
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL];
  STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM] 
INFERPSIGN_POS_EVEN_LEM);
  ASM_REWRITE_TAC[];
  EXISTS_TACL [`a`;`n`;`s`];
  (* save *)
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  ASM_MESON_TAC[];
  LABEL_ALL_TAC;
  CLAIM `
EVEN (
LENGTH sgns - 1)`;
  ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 = 
PRE x`];
  STRIP_TAC;
  ASM_SIMP_TAC[
DIV_EVEN];
  USE_THEN "Z-5" MP_TAC THEN ARITH_TAC;
]);;
 
let INFERPSIGN_NEG_EVEN_LEM = prove_by_refinement(
  `!a n p ps q qs r rs s x pts1 pts2  s1 s2 s3 rest sgns.
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (
LENGTH sgns = 2 * 
LENGTH pts1 + 1) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a <> &0) ==>
  
EVEN n ==>
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Neg s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `a pow n > &0`;
  ASM_MESON_TAC[
EVEN_ODD_POW];
  STRIP_TAC;
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[interpmat];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
  CASES_ON `pts1 = []`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;];
  COND_CASES_TAC;
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x < &0`;
  ASM_MESON_TAC[];
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x < &0`;
  ASM_MESON_TAC[];
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
  ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
  REPEAT STRIP_TAC;
  CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
     (CONS (\x'. 
LAST pts1 < x' /\ x' < x)
     (
TL (
partition_line (CONS x pts2))))) =
     (
APPEND
      (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x])
     (
TL (
partition_line (CONS x pts2))))`;
  ASM_MESON_TAC[
APPEND_CONS];
  DISCH_THEN (REWRITE_ALL o list);
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_ALL[
partition_line];
  COND_CASES_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  REWRITE_ALL[
TL;];
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  RESTRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x < &0`;
  ASM_MESON_TAC[];
  REPEAT_N 15 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  (* save *)
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 10 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x < &0`;
  ASM_MESON_TAC[];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 17 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT];
]);;
 
let INFERPSIGN_NEG_EVEN = prove_by_refinement(
  `!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a <> &0) ==>
  
EVEN n ==>
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Neg s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
APPEND sgns (CONS
    (
APPEND (CONS Unknown s1)
      (
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) =
        
LENGTH (
partition_line pts)`;
  REWRITE_ALL[interpmat];
  ASM_MESON_TAC[
ALL2_LENGTH];
  REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
  STRIP_TAC;
  TYPE_TACL (fun l -> MP_TAC (ISPECL l 
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
  STRIP_TAC;
  LABEL_ALL_TAC;
  PROVE_ASSUM_ANTECEDENT_TAC 0;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  ARITH_TAC;
  POP_ASSUM MP_TAC THEN STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `~(l2 = [])`;
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  REWRITE_ALL[
APPEND_NIL];
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL];
  STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM] 
INFERPSIGN_NEG_EVEN_LEM);
  ASM_REWRITE_TAC[];
  EXISTS_TACL [`a`;`n`;`s`];
  (* save *)
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  ASM_MESON_TAC[];
  LABEL_ALL_TAC;
  CLAIM `
EVEN (
LENGTH sgns - 1)`;
  ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 = 
PRE x`];
  STRIP_TAC;
  ASM_SIMP_TAC[
DIV_EVEN];
  USE_THEN "Z-5" MP_TAC THEN ARITH_TAC;
]);;
 
let INFERPSIGN_ZERO_EVEN_LEM = prove_by_refinement(
  `!a n p ps q qs r rs s x pts1 pts2  s1 s2 s3 rest sgns.
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (
LENGTH sgns = 2 * 
LENGTH pts1 + 1) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a <> &0) ==>
  
EVEN n ==>
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Zero s1)
        (
APPEND (CONS Zero s2) (CONS Zero s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `a pow n > &0`;
  ASM_MESON_TAC[
EVEN_ODD_POW];
  STRIP_TAC;
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[interpmat];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
  CASES_ON `pts1 = []`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;];
  COND_CASES_TAC;
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x = &0`;
  ASM_MESON_TAC[];
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x = &0`;
  ASM_MESON_TAC[];
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
  ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
  REPEAT STRIP_TAC;
  CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
     (CONS (\x'. 
LAST pts1 < x' /\ x' < x)
     (
TL (
partition_line (CONS x pts2))))) =
     (
APPEND
      (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x])
     (
TL (
partition_line (CONS x pts2))))`;
  ASM_MESON_TAC[
APPEND_CONS];
  DISCH_THEN (REWRITE_ALL o list);
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_ALL[
partition_line];
  COND_CASES_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  REWRITE_ALL[
TL;];
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  RESTRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x = &0`;
  ASM_MESON_TAC[];
  REPEAT_N 15 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  (* save *)
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 10 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x = &0`;
  ASM_MESON_TAC[];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 17 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
]);;
 
let INFERPSIGN_ZERO_EVEN = prove_by_refinement(
  `!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a <> &0) ==>
  
EVEN n ==>
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Zero s1)
        (
APPEND (CONS Zero s2) (CONS Zero s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
APPEND sgns (CONS
    (
APPEND (CONS Unknown s1)
      (
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) =
        
LENGTH (
partition_line pts)`;
  REWRITE_ALL[interpmat];
  ASM_MESON_TAC[
ALL2_LENGTH];
  REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
  STRIP_TAC;
  TYPE_TACL (fun l -> MP_TAC (ISPECL l 
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
  STRIP_TAC;
  LABEL_ALL_TAC;
  PROVE_ASSUM_ANTECEDENT_TAC 0;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  ARITH_TAC;
  POP_ASSUM MP_TAC THEN STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `~(l2 = [])`;
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  REWRITE_ALL[
APPEND_NIL];
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL];
  STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM] 
INFERPSIGN_ZERO_EVEN_LEM);
  ASM_REWRITE_TAC[];
  EXISTS_TACL [`a`;`n`;`s`];
  (* save *)
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  ASM_MESON_TAC[];
  LABEL_ALL_TAC;
  CLAIM `
EVEN (
LENGTH sgns - 1)`;
  ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 = 
PRE x`];
  STRIP_TAC;
  ASM_SIMP_TAC[
DIV_EVEN];
  USE_THEN "Z-5" MP_TAC THEN ARITH_TAC;
]);;
 
let INFERPSIGN_POS_ODD_POS_LEM = prove_by_refinement(
  `!a n p ps q qs r rs s x pts1 pts2  s1 s2 s3 rest sgns.
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (
LENGTH sgns = 2 * 
LENGTH pts1 + 1) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a > &0) ==>
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Pos s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `a pow n > &0`;
  ASM_MESON_TAC[
REAL_POW_LT;
real_gt;];
  STRIP_TAC;
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[interpmat];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
  CASES_ON `pts1 = []`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;];
  COND_CASES_TAC;
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x > &0`;
  ASM_MESON_TAC[];
  REPEAT_N 5 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x > &0`;
  ASM_MESON_TAC[];
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
  ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
  REPEAT STRIP_TAC;
  CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
     (CONS (\x'. 
LAST pts1 < x' /\ x' < x)
     (
TL (
partition_line (CONS x pts2))))) =
     (
APPEND
      (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x])
     (
TL (
partition_line (CONS x pts2))))`;
  ASM_MESON_TAC[
APPEND_CONS];
  DISCH_THEN (REWRITE_ALL o list);
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_ALL[
partition_line];
  COND_CASES_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  REWRITE_ALL[
TL;];
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  RESTRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x > &0`;
  ASM_MESON_TAC[];
  REPEAT_N 14 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`;
REAL_MUL_GT];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  (* save *)
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x > &0`;
  ASM_MESON_TAC[];
  REPEAT_N 15 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
]);;
 
let INFERPSIGN_POS_ODD_POS = prove_by_refinement(
  `!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a > &0) ==>
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Pos s1)
        (
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
APPEND sgns (CONS
    (
APPEND (CONS Unknown s1)
      (
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) =
        
LENGTH (
partition_line pts)`;
  REWRITE_ALL[interpmat];
  ASM_MESON_TAC[
ALL2_LENGTH];
  REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
  STRIP_TAC;
  TYPE_TACL (fun l -> MP_TAC (ISPECL l 
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
  STRIP_TAC;
  LABEL_ALL_TAC;
  PROVE_ASSUM_ANTECEDENT_TAC 0;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  ARITH_TAC;
  POP_ASSUM MP_TAC THEN STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `~(l2 = [])`;
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  REWRITE_ALL[
APPEND_NIL];
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL];
  STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM] 
INFERPSIGN_POS_ODD_POS_LEM);
  ASM_REWRITE_TAC[];
  EXISTS_TACL [`a`;`n`;`s`];
  (* save *)
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  ASM_MESON_TAC[];
  LABEL_ALL_TAC;
  CLAIM `
EVEN (
LENGTH sgns - 1)`;
  ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 = 
PRE x`];
  STRIP_TAC;
  ASM_SIMP_TAC[
DIV_EVEN];
  USE_THEN "Z-4" MP_TAC THEN ARITH_TAC;
]);;
 
let INFERPSIGN_NEG_ODD_POS_LEM = prove_by_refinement(
  `!a n p ps q qs r rs s x pts1 pts2  s1 s2 s3 rest sgns.
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (
LENGTH sgns = 2 * 
LENGTH pts1 + 1) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a > &0) ==>
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Neg s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `a pow n > &0`;
  ASM_MESON_TAC[
REAL_POW_LT;
real_gt;];
  STRIP_TAC;
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[interpmat];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
  CASES_ON `pts1 = []`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;];
  COND_CASES_TAC;
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x < &0`;
  ASM_MESON_TAC[
real_gt];
  REPEAT_N 5 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x < &0`;
  ASM_MESON_TAC[];
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
  ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
  REPEAT STRIP_TAC;
  CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
     (CONS (\x'. 
LAST pts1 < x' /\ x' < x)
     (
TL (
partition_line (CONS x pts2))))) =
     (
APPEND
      (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x])
     (
TL (
partition_line (CONS x pts2))))`;
  ASM_MESON_TAC[
APPEND_CONS];
  DISCH_THEN (REWRITE_ALL o list);
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_ALL[
partition_line];
  COND_CASES_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  REWRITE_ALL[
TL;];
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  RESTRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x < &0`;
  ASM_MESON_TAC[];
  REPEAT_N 14 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`;
REAL_MUL_GT];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  (* save *)
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x < &0`;
  ASM_MESON_TAC[];
  REPEAT_N 15 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
]);;
 
let INFERPSIGN_NEG_ODD_POS = prove_by_refinement(
  `!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a > &0) ==>
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Neg s1)
        (
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
APPEND sgns (CONS
    (
APPEND (CONS Unknown s1)
      (
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) =
        
LENGTH (
partition_line pts)`;
  REWRITE_ALL[interpmat];
  ASM_MESON_TAC[
ALL2_LENGTH];
  REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
  STRIP_TAC;
  TYPE_TACL (fun l -> MP_TAC (ISPECL l 
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
  STRIP_TAC;
  LABEL_ALL_TAC;
  PROVE_ASSUM_ANTECEDENT_TAC 0;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  ARITH_TAC;
  POP_ASSUM MP_TAC THEN STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `~(l2 = [])`;
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  REWRITE_ALL[
APPEND_NIL];
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL];
  STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM] 
INFERPSIGN_NEG_ODD_POS_LEM);
  ASM_REWRITE_TAC[];
  EXISTS_TACL [`a`;`n`;`s`];
  (* save *)
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  ASM_MESON_TAC[];
  LABEL_ALL_TAC;
  CLAIM `
EVEN (
LENGTH sgns - 1)`;
  ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 = 
PRE x`];
  STRIP_TAC;
  ASM_SIMP_TAC[
DIV_EVEN];
  USE_THEN "Z-4" MP_TAC THEN ARITH_TAC;
]);;
 
let INFERPSIGN_ZERO_ODD_POS_LEM = prove_by_refinement(
  `!a n p ps q qs r rs s x pts1 pts2  s1 s2 s3 rest sgns.
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (
LENGTH sgns = 2 * 
LENGTH pts1 + 1) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a > &0) ==>
  interpmat (
APPEND pts1 (CONS x pts2))
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Zero s1)
        (
APPEND (CONS Zero s2) (CONS Zero s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `a pow n > &0`;
  ASM_MESON_TAC[
REAL_POW_LT;
real_gt;];
  STRIP_TAC;
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[interpmat];
  REPEAT STRIP_TAC;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
  CASES_ON `pts1 = []`;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;];
  COND_CASES_TAC;
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x = &0`;
  ASM_MESON_TAC[
real_gt];
  REPEAT_N 5 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 6 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
  CLAIM `?k. sgns = [k]`;
  MATCH_EQ_MP_TAC (GSYM 
LENGTH_1);
  REWRITE_ALL[
LENGTH];
  REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
  REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_ALL[interpsigns;interpsign;
ALL2;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x = &0`;
  ASM_MESON_TAC[];
  REPEAT_N 7 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
  ASM_REWRITE_TAC[];
  (* save *)
  POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
  ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
  REPEAT STRIP_TAC;
  CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
     (CONS (\x'. 
LAST pts1 < x' /\ x' < x)
     (
TL (
partition_line (CONS x pts2))))) =
     (
APPEND
      (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x])
     (
TL (
partition_line (CONS x pts2))))`;
  ASM_MESON_TAC[
APPEND_CONS];
  DISCH_THEN (REWRITE_ALL o list);
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_ALL[
partition_line];
  COND_CASES_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REPEAT STRIP_TAC;
  REWRITE_ALL[
TL;];
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REPEAT_N 8 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  RESTRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x = &0`;
  ASM_MESON_TAC[];
  REPEAT_N 14 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`;
REAL_MUL_GT;
REAL_LT_IMP_NZ];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  (* save *)
  CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
      [\x'. 
LAST pts1 < x' /\ x' < x]) = 
LENGTH sgns`;
  FIRST_ASSUM (MP_TAC o MATCH_MP  
ALL2_LENGTH);
  ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
  ARITH_TAC;
  STRIP_TAC;
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REPEAT STRIP_TAC;
  MATCH_MP_TAC 
ALL2_APPEND;
  ASM_REWRITE_TAC[];
  (* save *)
  REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
  ASM_REWRITE_TAC[];
  REPEAT STRIP_TAC;
  REPEAT_N 9 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
  REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  REPEAT_N 4 (POP_ASSUM MP_TAC);
  POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
  FIRST_ASSUM (MP_TAC o MATCH_MP 
ALL2_APPEND_LENGTH);
  FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
  REWRITE_TAC[
ALL2;interpsign;];
  REPEAT STRIP_TAC;
  REWRITE_ALL[interpsigns;
ALL2;interpsign;];
  ASM_REWRITE_TAC[];
  CLAIM `q x = &0`;
  ASM_MESON_TAC[];
  CLAIM `r x = &0`;
  ASM_MESON_TAC[];
  REPEAT_N 15 (POP_ASSUM MP_TAC);
  POP_ASSUM (MP_TAC o ISPEC `x:real`);
  REPEAT STRIP_TAC;
  POP_ASSUM (REWRITE_ALL o list);
  REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
  REPEAT_N 16 (POP_ASSUM MP_TAC);
  POP_ASSUM (REWRITE_ALL o list o GSYM);
  REWRITE_TAC[
real_gt;
REAL_MUL_GT];
  REPEAT STRIP_TAC;
  ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`;
REAL_MUL_GT;
REAL_LT_IMP_NZ];
]);;
 
let INFERPSIGN_ZERO_ODD_POS = prove_by_refinement(
  `!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Unknown s1)
        (
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) ==>
  (
LENGTH ps = 
LENGTH s1) ==>
  (
LENGTH qs = 
LENGTH s2) ==>
  
ODD (
LENGTH sgns) ==>
  (!x. a pow n * p x = s x * q x + r x) ==>
  (a > &0) ==>
  interpmat pts
    (
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
    (
APPEND sgns
      (CONS (
APPEND (CONS Zero s1)
        (
APPEND (CONS Zero s2) (CONS Zero s3))) rest))`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  CLAIM `
LENGTH (
APPEND sgns (CONS
    (
APPEND (CONS Unknown s1)
      (
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) =
        
LENGTH (
partition_line pts)`;
  REWRITE_ALL[interpmat];
  ASM_MESON_TAC[
ALL2_LENGTH];
  REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
  STRIP_TAC;
  TYPE_TACL (fun l -> MP_TAC (ISPECL l 
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
  STRIP_TAC;
  LABEL_ALL_TAC;
  PROVE_ASSUM_ANTECEDENT_TAC 0;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC;
  ARITH_TAC;
  POP_ASSUM MP_TAC THEN STRIP_TAC;
  ASM_REWRITE_TAC[];
  CLAIM `~(l2 = [])`;
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  REWRITE_ALL[
APPEND_NIL];
  POP_ASSUM (REWRITE_ALL o list);
  POP_ASSUM (fun x -> ALL_TAC);
  DISCH_THEN (REWRITE_ALL o list);
  POP_ASSUM MP_TAC;
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM (fun x -> ALL_TAC);
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  REWRITE_TAC[
NOT_NIL];
  STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
  MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM] 
INFERPSIGN_ZERO_ODD_POS_LEM);
  ASM_REWRITE_TAC[];
  EXISTS_TACL [`a`;`n`;`s`];
  (* save *)
  ASM_REWRITE_TAC[];
  STRIP_TAC;
  ASM_MESON_TAC[];
  LABEL_ALL_TAC;
  CLAIM `
EVEN (
LENGTH sgns - 1)`;
  ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 = 
PRE x`];
  STRIP_TAC;
  ASM_SIMP_TAC[
DIV_EVEN];
  USE_THEN "Z-4" MP_TAC THEN ARITH_TAC;
]);;