Theory Hybrid_Multiv_Algorithm_Proofs

(* This file includes proofs (soundness and completeness) for our 
  top-level hybrid QE algorithm defined in Hybrid_Multiv_Algorithm.thy.
*)


theory Hybrid_Multiv_Algorithm_Proofs

imports Hybrid_Multiv_Algorithm
  Hybrid_Multiv_Matrix_Proofs
  Virtual_Substitution.ExportProofs

begin

subsection "Lemmas about branching (lc assump generation)"

lemma lc_assump_generation_induct[case_names Base Rec Lookup0 LookupN0]:
  fixes q :: "real mpoly Polynomial.poly"
  fixes assumps ::"(real mpoly × rat) list"
  assumes base: "⋀q assumps. q = 0 ⟹ P q assumps"
    and rec: "⋀q assumps.
        ⟦q ≠ 0;
        lookup_assump_aux (Polynomial.lead_coeff q) assumps = None;
        P (one_less_degree q) ((Polynomial.lead_coeff q, 0) # assumps)⟧ ⟹
        P q assumps"
    and lookup0: "⋀q assumps.
        ⟦q ≠ 0;
        lookup_assump_aux (Polynomial.lead_coeff q) assumps = Some 0;
        P (one_less_degree q) assumps⟧ ⟹ P q assumps"
    and lookupN0: "⋀q assumps r. 
        ⟦q ≠ 0;
        lookup_assump_aux (Polynomial.lead_coeff q) assumps = Some r;
        r ≠ 0⟧ ⟹ P q assumps"
  shows "P q assumps"
  apply(induct q assumps rule: lc_assump_generation.induct)
  by (metis base rec lookup0 lookupN0 not_None_eq)


lemma lc_assump_generation_subset:
  assumes "(branch_assms, branch_poly_list) ∈ set(lc_assump_generation q assumps)"
  shows "set assumps ⊆ set branch_assms"
  using assms 
proof (induct q assumps rule: lc_assump_generation_induct)
  case (Base q assumps)
  then show ?case 
    by (auto simp add: lc_assump_generation.simps)
next
  case (Rec q assumps)
  let ?zero = "lc_assump_generation (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # assumps)"
  let ?one  = "((Polynomial.lead_coeff q, (1::rat)) # assumps, q)"
  let ?minus_one  = "((Polynomial.lead_coeff q, (-1::rat)) # assumps, q)"
  have "(branch_assms, branch_poly_list) ∈ set (?one#?minus_one#?zero)"
    using Rec.hyps Rec(4) lc_assump_generation.simps by auto 
  then show ?case
    using Rec(3) by force  
next
  case (Lookup0 q assumps)
  then show ?case 
    using lc_assump_generation.simps
    by simp 
next
  case (LookupN0 q assumps r)
  then show ?case 
    by (auto simp add: lc_assump_generation.simps)
qed

lemma branch_init_assms_subset:
  assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
  shows "set init_assumps ⊆ set branch_assms"
  using assms
proof (induct qs arbitrary: branch_assms branch_poly_list init_assumps)
  case Nil
  then show ?case
    by (simp add: lc_assump_generation_list.simps(1))
next
  case (Cons a bpl)
  then show ?case
    using lc_assump_generation_subset 
    apply (auto simp add: lc_assump_generation_list.simps)
    by blast
qed

lemma prod_list_var_gen_nonzero:
  shows "prod_list_var_gen qs ≠ 0"
proof (induct qs)
  case Nil
  then show ?case by auto
next
  case (Cons a qs)
  then show ?case by auto 
qed

(* Invariant: For all (a, q) in the output, either
  q is 0 or the leading coefficient of q is assumed nonzero in a *)
lemma lc_assump_generation_inv:
  assumes "(a, q) ∈ set (lc_assump_generation init_q assumps)"
  shows "q = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff q) a = Some i ∧ i ≠ 0))"
  using assms
proof (induct init_q assumps arbitrary: q a rule: lc_assump_generation_induct )
  case (Base init_q assumps)
  then show ?case 
    using lc_assump_generation.simps by auto 
next
  case (Rec init_q assumps)
  let ?zero = "lc_assump_generation (one_less_degree init_q) ((Polynomial.lead_coeff init_q, (0::rat)) # assumps)"
  let ?one  = "((Polynomial.lead_coeff init_q, (1::rat)) # assumps, init_q)"
  let ?minus_one = "((Polynomial.lead_coeff init_q, (-1::rat)) # assumps, init_q)"
  have "(a, q) ∈ set (?one # ?minus_one # ?zero)"
    using Rec.prems Rec.hyps(1) Rec.hyps(2) lc_assump_generation.simps
    by auto
  then have eo: "(a, q) = ?one ∨ (a, q) = ?minus_one ∨ (a, q) ∈ set(?zero)"
    by auto
  {assume *: "(a, q) = ?one"
    then have "q = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff q) a = Some i ∧ i ≠ 0))"
      by auto
  }
  moreover {assume *: "(a, q) = ?minus_one"
    then have "q = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff q) a = Some i ∧ i ≠ 0))"
      by auto
  }
  moreover   {assume *: "(a, q)  ∈ set(?zero)"
    then have "q = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff q) a = Some i ∧ i ≠ 0))"
      using Rec.hyps Rec.prems by auto
  }
  ultimately show ?case 
    using lc_assump_generation.simps
    using eo by fastforce
next
  case (Lookup0 init_q assumps)
  then show ?case using lc_assump_generation.simps by auto 
next
  case (LookupN0 init_q assumps r)
  then show ?case using lc_assump_generation.simps by auto 
qed

lemma lc_assump_generation_list_inv:
  assumes val: "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
  assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
  shows "q ∈ set branch_poly_list ⟹ q = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff q) branch_assms = Some i ∧ i ≠ 0)"
  using assms
proof (induct qs arbitrary: q init_assumps branch_poly_list branch_assms)
  case Nil
  then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
    using lc_assump_generation_list.simps by auto
  then have "branch_poly_list = []"
    using in_set_member
    by simp 
  then show ?case 
    using Nil.prems(1)
    by simp  
next
  case (Cons a qs)
  let ?rec = "lc_assump_generation a init_assumps"
  have inset: "(branch_assms,branch_poly_list) ∈ set (
    concat (map (
      λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
    using Cons.prems lc_assump_generation_list.simps
    by auto 
  then obtain new_assumps r where deconstruct_prop:
    "(new_assumps, r) ∈ set ?rec"
    "(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec)"
    using inset
    by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
  then obtain elem list_rec where list_rec_prop:
    "list_rec = lc_assump_generation_list qs new_assumps"
    "elem ∈ set list_rec"
    "(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))" 
    by auto
  then have pair_in_set: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
    using deconstruct_prop by auto
  then have snd_elem_is: "⋀q. q ∈ set (snd elem) ⟹
    q = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff q) branch_assms = Some i ∧ i ≠ 0)"
    using Cons.hyps
    by (simp add: local.Cons(3)) 
  have ris_var: "r = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff r)new_assumps = Some i ∧ i ≠ 0) "
    using lc_assump_generation_inv[of new_assumps r a init_assumps] deconstruct_prop(1) 
    by auto
  have "set new_assumps ⊆ set branch_assms"
    using deconstruct_prop list_rec_prop
    using pair_in_set branch_init_assms_subset by presburger
  then have "(∃i. lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i ∧ i ≠ 0) ⟹
(∃i. lookup_assump_aux (Polynomial.lead_coeff r) branch_assms = Some i ∧ i ≠ 0)"
    using val lookup_assump_aux_subset_consistency
    using local.Cons(3) by blast
  then have ris: "r = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff r) branch_assms = Some i ∧ i ≠ 0) "
    using ris_var by auto
  then show ?case
    using ris snd_elem_is list_rec_prop(3)
    using Cons.prems(1) by auto
qed

subsection "Correctness of sign determination inner"

lemma q_dvd_prod_list_var_prop:
  assumes "q ∈ set qs"
  assumes "q ≠ 0"
  shows "q dvd prod_list_var_gen qs" using assms
proof (induct qs)
  case Nil
  then show ?case by auto
next
  case (Cons a qs)
  then have eo: "q = a ∨q ∈ set qs" by auto
  have c1: "q = a ⟹ q dvd prod_list_var_gen (a#qs)"
  proof - 
    assume "q = a"
    then have "prod_list_var_gen (a#qs) = q*(prod_list_var_gen qs)" using Cons.prems
      unfolding prod_list_var_gen_def by auto
    then show ?thesis using prod_list_var_gen_nonzero[of qs] by auto
  qed
  have c2: "q ∈ set qs ⟶ q dvd prod_list_var_gen qs"
    using Cons.prems Cons.hyps unfolding prod_list_var_gen_def by auto
  show ?case using eo c1 c2 by auto
qed

lemma poly_p_nonzero_on_branch:
  assumes assms: "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
  assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
  assumes "p = poly_p_in_branch (branch_assms, branch_poly_list)"
  shows "eval_mpoly_poly val p ≠ 0"
proof - 
  (* Some intuition: the assumps on the qs are contained in branch_assms,
    then because branch_assms contains the proper assumps,
    the poly_p_in_branch definition correctly handles things *)
  {assume *: "(check_all_const_deg_gen branch_poly_list = True)"
    then have p_is: "p = [:0, 1:]"
      using assms
      using poly_p_in_branch.simps by presburger 
    then have "eval_mpoly_poly val p ≠ 0"
      by (metis Polynomial.lead_coeff_monom degree_0 dvd_refl eval_commutes eval_mpoly_map_poly_comm_ring_hom.base.hom_one not_is_unit_0 poly_dvd_1 x_as_monom)
  }
  moreover {assume *: "(check_all_const_deg_gen branch_poly_list = False)"
    then have p_is: "p = (pderiv (prod_list_var_gen branch_poly_list)) * (prod_list_var_gen branch_poly_list)"
      using assms
      using poly_p_in_branch.simps by presburger 
    then have assms_inv: "⋀q. q ∈ set branch_poly_list ⟹ q = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff q) branch_assms = Some i ∧ i ≠ 0)"
      using lc_assump_generation_list_inv assms
      by (meson assms(2)) 
    have q_inv: "⋀q. q ∈ set branch_poly_list ⟹ q ≠ 0 ⟹ eval_mpoly_poly val q ≠ 0"
      using assms_inv assms 
      by (metis eval_commutes leading_coeff_0_iff lookup_assum_aux_mem satisfies_evaluation_nonzero)
    then have "⋀q. q ∈ set branch_poly_list ⟹ (q ≠ 0 ⟷ eval_mpoly_poly val q ≠ 0)"
      by auto
    then have prod_list_eval: "(eval_mpoly_poly val (prod_list_var_gen branch_poly_list)) = (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list))"
    proof (induct branch_poly_list)
      case Nil
      then show ?case by auto
    next
      case (Cons a branch_poly_list)
      { assume *: "a = 0"
        then have h1: "eval_mpoly_poly val (prod_list_var_gen (a # branch_poly_list)) = 
          eval_mpoly_poly val (prod_list_var_gen branch_poly_list)"
          by simp
        have "eval_mpoly_poly val a = 0"
          using * by auto 
        then have h2: "prod_list_var_gen (map (eval_mpoly_poly val) (a # branch_poly_list))
      = prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)"
          by auto
        then have "eval_mpoly_poly val (prod_list_var_gen (a # branch_poly_list)) =
       prod_list_var_gen (map (eval_mpoly_poly val) (a # branch_poly_list))"
          using Cons.hyps Cons.prems h1 h2
          by (simp add: member_rec(1)) 
      }
      moreover { assume *: "a ≠ 0"
        then have h1: "eval_mpoly_poly val (prod_list_var_gen (a # branch_poly_list)) = 
          (eval_mpoly_poly val a)*(eval_mpoly_poly val (prod_list_var_gen branch_poly_list))"
          by (simp add: eval_mpoly_poly_comm_ring_hom.hom_mult)
        have "eval_mpoly_poly val a ≠ 0"
          using * assms Cons.prems
          by (meson list.set_intros(1))
        then have h2: "prod_list_var_gen (map (eval_mpoly_poly val) (a # branch_poly_list))
          = (eval_mpoly_poly val a)* prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)"
          by auto
        have "eval_mpoly_poly val (prod_list_var_gen (a # branch_poly_list)) =
          prod_list_var_gen (map (eval_mpoly_poly val) (a # branch_poly_list))"
          using Cons.hyps Cons.prems h1 h2
          by (simp add: member_rec(1)) 
      }
      ultimately show ?case 
        by auto 
    qed
    have degree_q_inv: "⋀q. q ∈ set branch_poly_list ⟹ q ≠ 0 ⟹ Polynomial.degree (eval_mpoly_poly val q) = Polynomial.degree q"
      using assms_inv assms q_inv
      by (metis degree_valuation lookup_assum_aux_mem) 
    have prod_nonz: "eval_mpoly_poly val (prod_list_var_gen branch_poly_list) ≠ 0"
      using q_inv prod_list_eval
      by (simp add: prod_list_var_gen_nonzero)
    have ex_q: "∃q ∈ set branch_poly_list. (q ≠ 0 ∧ Polynomial.degree q > 0)"
      using * proof (induct branch_poly_list)
      case Nil
      then show ?case by auto
    next
      case (Cons a branch_poly_list)
      then show ?case
        by (metis bot_nat_0.not_eq_extremum check_all_const_deg_gen.simps(2) degree_0 list.set_intros(1) list.set_intros(2))
    qed
    obtain pos_deg_poly where pos_deg_poly: "pos_deg_poly∈set branch_poly_list ∧ pos_deg_poly ≠ 0 ∧ 0 < Polynomial.degree pos_deg_poly"
      using ex_q by blast 
    have "pos_deg_poly dvd (prod_list_var_gen branch_poly_list)"
      by (simp add: Hybrid_Multiv_Algorithm_Proofs.q_dvd_prod_list_var_prop pos_deg_poly)
    then have nonc_dvd: "(eval_mpoly_poly val pos_deg_poly) dvd (eval_mpoly_poly val (prod_list_var_gen branch_poly_list))"
      by blast
    have "Polynomial.degree (eval_mpoly_poly val pos_deg_poly) > 0"
      using pos_deg_poly degree_q_inv
      by metis 
    then have prod_nonc:"Polynomial.degree (eval_mpoly_poly val (prod_list_var_gen branch_poly_list)) ≠ 0"
      using  nonc_dvd prod_nonz
      by (metis bot_nat_0.extremum_strict dvd_const) 
    then have "eval_mpoly_poly val p ≠ 0"
      using prod_nonz prod_nonc
      by (metis eval_mpoly_poly_comm_ring_hom.hom_mult no_zero_divisors p_is pderiv_commutes pderiv_eq_0_iff) 
  }
  ultimately show ?thesis by auto
qed

lemma calc_data_to_signs_and_extract_signs:
  shows "(calculate_data_to_signs ell) = extract_signs ell"
  by auto

lemma branch_poly_eval:
  assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
  assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
  shows "(eval_mpoly_poly val) q = (eval_mpoly_poly val) init_q"
  using assms 
proof (induct init_q init_assumps arbitrary: q a rule: lc_assump_generation_induct )
  case (Base init_q init_assumps)
  then show ?case
    by (simp add: lc_assump_generation.simps) 
next
  case (Rec init_q init_assumps)
  then show ?case using lc_assump_generation.simps
      basic_trans_rules(31) eval_mpoly_poly_one_less_degree in_set_member lc_assump_generation_subset member_rec(1) option.case(1) prod.inject
    by (smt (verit, best))
next
  case (Lookup0 init_q init_assumps)
  then show ?case 
    using lc_assump_generation.simps
    by (smt (z3) eval_mpoly_poly_one_less_degree lc_assump_generation_subset lookup_assum_aux_mem option.simps(5) subset_eq) 
      (* Takes a second to load *)
next
  case (LookupN0 init_q init_assumps r)
  then show ?case
    by (simp add: lc_assump_generation.simps) 
qed

lemma eval_prod_list_var_gen_match:
  assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
  assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
  shows "eval_mpoly_poly val (prod_list_var_gen branch_poly_list) =
    prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)"
  using assms 
proof (induct qs arbitrary: branch_assms branch_poly_list init_assumps val)
  case Nil
  then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
    using lc_assump_generation_list.simps by auto
  then have "branch_poly_list = []"
    using in_set_member
    by simp
  then show ?case
    by simp
next
  case (Cons a qs)
  let ?rec = "lc_assump_generation a init_assumps"
  have inset: "(branch_assms,branch_poly_list) ∈ set (
    concat (map (
      λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
    using Cons.prems lc_assump_generation_list.simps
    by auto 
  then obtain new_assumps r where deconstruct_prop:
    "(new_assumps, r) ∈ set ?rec"
    "(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec)"
    using inset
    by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
  then obtain elem list_rec where list_rec_prop:
    "list_rec = lc_assump_generation_list qs new_assumps"
    "elem ∈ set list_rec"
    "(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))" 
    by auto
  then have branch_assms_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
    using deconstruct_prop by auto
  then have "set new_assumps ⊆ set branch_assms"
    using deconstruct_prop list_rec_prop branch_init_assms_subset
    by presburger
  have ris_var: "r = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff r)new_assumps = Some i ∧ i ≠ 0) "
    using lc_assump_generation_inv[of new_assumps r a init_assumps] deconstruct_prop(1) 
    by auto
  then have r_prop: "r = 0 ⟷ eval_mpoly_poly val r = 0"
    by (metis ‹set new_assumps ⊆ set branch_assms› basic_trans_rules(31) eval_commutes eval_mpoly_poly_comm_ring_hom.hom_zero leading_coeff_0_iff local.Cons(3) lookup_assum_aux_mem satisfies_evaluation_nonzero)
  have "eval_mpoly_poly val (prod_list_var_gen (snd elem)) =
    prod_list_var_gen (map (eval_mpoly_poly val) (snd elem))"
    using Cons.hyps list_rec_prop
    using branch_assms_inset local.Cons(3) by blast 
  then show ?case using r_prop list_rec_prop(3)
    by (simp add: eval_mpoly_poly_comm_ring_hom.hom_mult) 
qed

lemma map_branch_poly_list:
  assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
  assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
  shows "(map (eval_mpoly_poly val) qs) = (map (eval_mpoly_poly val) branch_poly_list)"
  using assms 
proof (induct qs arbitrary: branch_assms branch_poly_list init_assumps)
  case Nil
  then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
    using lc_assump_generation_list.simps by auto
  then have "branch_poly_list = []"
    using in_set_member
    by simp 
  then show ?case 
    using Nil.prems(1)
    by meson 
next
  case (Cons a qs)
  let ?rec = "lc_assump_generation a init_assumps"
  have inset: "(branch_assms,branch_poly_list) ∈ set (
    concat (map (
      λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
    using Cons.prems lc_assump_generation_list.simps
    by auto 
  then obtain new_assumps r where deconstruct_prop:
    "(new_assumps, r) ∈ set ?rec"
    "(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec)"
    using inset
    by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
  then obtain elem list_rec where list_rec_prop:
    "list_rec = lc_assump_generation_list qs new_assumps"
    "elem ∈ set list_rec"
    "(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))" 
    by auto
  then have branch_assms_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
    using deconstruct_prop by auto
  then have map_prop: "map (eval_mpoly_poly val) (qs) =
    map (eval_mpoly_poly val) (snd elem)" using Cons.hyps Cons.prems
    by blast
  have "set new_assumps ⊆ set branch_assms"
    using deconstruct_prop list_rec_prop branch_assms_inset branch_init_assms_subset 
    by presburger
  then have "eval_mpoly_poly val r = eval_mpoly_poly val a"
    using branch_poly_eval
    by (meson basic_trans_rules(31) deconstruct_prop(1) local.Cons(3)) 
  then show ?case 
    using map_prop list_rec_prop(3)
    by simp 
qed

lemma check_constant_degree_match:
  assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
  assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
  shows "Polynomial.degree q = Polynomial.degree (eval_mpoly_poly val init_q)"
  using assms 
proof (induct init_q init_assumps arbitrary: q a rule: lc_assump_generation_induct )
  case (Base init_q init_assumps)
  then show ?case 
    using lc_assump_generation.simps
    by simp 
next
  case (Rec init_q init_assumps)
  then show ?case using lc_assump_generation.simps
    by (metis branch_poly_eval degree_0 degree_valuation eval_mpoly_poly_comm_ring_hom.hom_zero lc_assump_generation_inv lookup_assum_aux_mem) 
next
  case (Lookup0 init_q init_assumps)
  then show ?case  using lc_assump_generation.simps
    by (metis branch_poly_eval degree_0 degree_valuation eval_mpoly_poly_comm_ring_hom.hom_zero lc_assump_generation_inv lookup_assum_aux_mem) 
next
  case (LookupN0 init_q init_assumps r)
  then show ?case
    using lc_assump_generation.simps
    by (metis branch_poly_eval degree_0 degree_valuation eval_mpoly_poly_comm_ring_hom.hom_zero lc_assump_generation_inv lookup_assum_aux_mem) 
qed

lemma check_constant_degree_match_list:
  assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
  assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
  shows "(check_all_const_deg_gen branch_poly_list) = (check_all_const_deg_gen (map (eval_mpoly_poly val) qs))"
  using assms
proof (induct qs arbitrary: branch_assms branch_poly_list init_assumps)
  case Nil
  then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
    using lc_assump_generation_list.simps
    by auto
  then have "branch_poly_list = []"
    using in_set_member
    by simp 
  then show ?case
    by simp 
next
  case (Cons a qs)
  let ?rec = "lc_assump_generation a init_assumps"
  have inset: "(branch_assms,branch_poly_list) ∈ set (
    concat (map (
      λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
    using Cons.prems lc_assump_generation_list.simps
    by auto 
  then obtain new_assumps r where deconstruct_prop:
    "(new_assumps, r) ∈ set ?rec"
    "(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec)"
    using inset
    by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
  then obtain elem list_rec where list_rec_prop:
    "list_rec = lc_assump_generation_list qs new_assumps"
    "elem ∈ set list_rec"
    "(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))" 
    by auto
  then have branch_assms_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
    using deconstruct_prop by auto
  then have ind_prop: "(check_all_const_deg_gen (snd elem)) = (check_all_const_deg_gen (map (eval_mpoly_poly val) qs))" using Cons.hyps Cons.prems
    by blast
  have "set new_assumps ⊆ set branch_assms"
    using deconstruct_prop list_rec_prop branch_assms_inset branch_init_assms_subset 
    by presburger
  then have "Polynomial.degree r = Polynomial.degree (eval_mpoly_poly val a)"
    using check_constant_degree_match
    by (meson basic_trans_rules(31) deconstruct_prop(1) local.Cons(3)) 
  then show ?case 
    using ind_prop list_rec_prop(3)
    by simp 
qed

lemma check_all_const_deg_match:
  shows "check_all_const_deg qs = check_all_const_deg_gen qs"
proof (induct qs)
  case Nil
  then show ?case by auto
next
  case (Cons a qs)
  then show ?case by auto
qed

lemma prod_list_var_match:
  shows "prod_list_var_gen qs = prod_list_var qs"
proof (induct qs)
  case Nil
  then show ?case by auto
next
  case (Cons a qs)
  then show ?case by auto
qed

lemma sign_lead_coeff_on_branch:
  assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
  assumes "q ≠ 0"
  assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
  shows "((Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))) = 
   Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q))"
  using assms 
proof (induct init_q init_assumps arbitrary: q a rule: lc_assump_generation_induct )
  case (Base init_q init_assumps)
  then show ?case using lc_assump_generation.simps
    by simp 
next
  case (Rec init_q init_assumps)
  let ?zero = "lc_assump_generation (one_less_degree init_q) ((Polynomial.lead_coeff init_q, (0::rat)) # init_assumps)"
  let ?one  = "((Polynomial.lead_coeff init_q, (1::rat)) # init_assumps, init_q)"
  let ?minus_one  = "((Polynomial.lead_coeff init_q, (-1::rat)) # init_assumps, init_q)"
  have inset: "(a, q) ∈ set (?one#?minus_one#?zero)"
    using Rec.hyps lc_assump_generation.simps Rec(4)
    by auto 
  { assume * : "(a, q) = ?one"
    then have h1: "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) = (1::rat)"
      by auto
    have h2: "satisfies_evaluation val (Polynomial.lead_coeff q) (1)"
      using Rec.hyps
      by (metis "*" Pair_inject Rec.prems(3) list.set_intros(1)) 
    then have h3: "Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q)) = (1::int)"
      unfolding satisfies_evaluation_def eval_mpoly_def
      by (metis Sturm_Tarski.sign_def h2 lead_coeff_valuation of_int_hom.injectivity one_neq_zero satisfies_evaluation_def verit_comp_simplify(28))
        (* may take a second to load *)
    have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) = 
      ((Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q))))"
      using h1 h3 
      by auto
  } moreover { 
    assume * : "(a, q) = ?minus_one"
    then have h1: "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) = (-1::rat)"
      by auto
    have h2: "satisfies_evaluation val (Polynomial.lead_coeff q) (-1)"
      using Rec.hyps
      by (metis "*" Pair_inject Rec.prems(3) list.set_intros(1)) 
    then have h3: "rat_of_int (Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q))) = (-1::rat)"
      unfolding satisfies_evaluation_def eval_mpoly_def
      by (metis Sturm_Tarski.sign_def degree_valuation eval_mpoly_def eval_mpoly_map_poly_comm_ring_hom.base.coeff_map_poly_hom eval_mpoly_poly_def h2 of_int_hom.hom_one of_int_hom.injectivity of_int_minus rel_simps(88) sign_uminus verit_comp_simplify(28))
        (* May take a second to load *)
    have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) = 
      ((Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q))))"
      using h1 h3
      by (metis of_int_eq_iff of_rat_of_int_eq) 
  }
  moreover { 
    assume * : "(a, q) ∈ set ?zero"
    then have "(a, q)
    ∈ set (lc_assump_generation (Multiv_Poly_Props.one_less_degree init_q)
             ((Polynomial.lead_coeff init_q, 0) # init_assumps))"
      by auto 
    then have "set ((Polynomial.lead_coeff init_q, 0) # init_assumps) ⊆ set a "
      using lc_assump_generation_subset by presburger 
    then have "⋀p n. (p, n) ∈ set ((Polynomial.lead_coeff init_q, 0) # init_assumps) ⟹ satisfies_evaluation val p n"
      using Rec.prems by auto 
    then have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) = 
      Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q))"
      using Rec.hyps Rec.prems
      by (smt (verit, ccfv_SIG) "*" Sturm_Tarski.sign_cases more_arith_simps(10) neg_one_neq_one sign_uminus) 
      (* Takes a couple seconds to load *)
  }
  ultimately show ?case using lc_assump_generation.simps
      inset 
    by (smt (verit, del_insts) set_ConsD) (* Takes a second *)
next
  case (Lookup0 init_q init_assumps)
  then show ?case using lc_assump_generation.simps
    by auto

next
  case (LookupN0 init_q init_assumps r)
  then have match: "(a, q) = (init_assumps, init_q)"
    using lc_assump_generation.simps in_set_member by auto 
  then obtain i where i_prop: "i ≠ 0"
    "lookup_assump_aux (Polynomial.lead_coeff init_q) init_assumps = Some i"
    "(Polynomial.lead_coeff init_q, i) ∈ set init_assumps"
    using LookupN0.prems LookupN0.hyps
    by (meson lookup_assum_aux_mem)  
  then have "(Polynomial.lead_coeff init_q, i) ∈ set a"
    using match by auto
  then have sat_eval: "satisfies_evaluation val (Polynomial.lead_coeff init_q) i"
    using LookupN0(6) by blast
  have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a)
   = Sturm_Tarski.sign i"
    using i_prop match lookup_assump_aux_subset_consistent_sign
    by simp
  then show ?case
    by (smt (verit, del_insts) LookupN0(6) LookupN0.prems(1) sat_eval branch_poly_eval i_prop(1) lead_coeff_valuation of_int_hom.injectivity satisfies_evaluation_def) 
qed

lemma sign_lead_coeff_on_branch_init:
  assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
  assumes "q ≠ 0"
  assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
  shows "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) = 
   Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val init_q))"
  using sign_lead_coeff_on_branch branch_poly_eval
  by (metis assms(1) assms(2) assms(3)) 

lemma pos_limit_point_on_branch:
  assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
  assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
  shows "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val q))) = 
     (if q = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))"
  using assms 
proof - 
  have "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val q))) = 
    Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q)) "
    unfolding sgn_pos_inf_def
    by auto
  then show ?thesis using sign_lead_coeff_on_branch assms
    by (smt (verit, del_insts) eval_mpoly_poly_comm_ring_hom.hom_zero leading_coeff_0_iff sign_simps(2))
      (* May take a few seconds to load *)
qed

lemma pos_limit_point_on_branch_init:
  assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
  assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
  shows "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val init_q))) = 
     (if q = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))"
  using assms pos_limit_point_on_branch  sign_lead_coeff_on_branch_init
  using branch_poly_eval by force

lemma pos_limit_point_on_branch_list:
  assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
  assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
  assumes "(pos_limit_branch, neg_limit_branch) = limit_points_on_branch (branch_assms, branch_poly_list)"
  shows "map rat_of_int (sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs)) = pos_limit_branch"
  using assms 
proof (induct qs arbitrary: pos_limit_branch neg_limit_branch branch_assms branch_poly_list init_assumps)
  case Nil
  then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
    using lc_assump_generation_list.simps
    by auto
  then have "branch_poly_list = []"
    using in_set_member
    by simp 
  then show ?case using Nil.prems 
    unfolding eval_mpoly_poly_def sgn_pos_inf_rat_list_def
    by auto
next
  case (Cons a qs) 
  let ?rec = "lc_assump_generation a init_assumps"
  have inset: "(branch_assms,branch_poly_list) ∈ set (
    concat (map (
      λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
    using Cons.prems lc_assump_generation_list.simps
    by auto 
  then obtain new_assumps r where deconstruct_prop:
    "(new_assumps, r) ∈ set ?rec"
    "(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec)"
    using inset
    by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
  then obtain elem list_rec where list_rec_prop:
    "list_rec = lc_assump_generation_list qs new_assumps"
    "elem ∈ set list_rec"
    "(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))" 
    by auto
  then have snd_elem_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
    using deconstruct_prop by auto
  obtain pos_limit_sublist neg_limit_sublist where sublist_prop:
    "(pos_limit_sublist, neg_limit_sublist) = limit_points_on_branch (branch_assms, snd elem)"
    by auto 
  then have ind_prop: "pos_limit_sublist = map rat_of_int (sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs))"
    using snd_elem_inset Cons.hyps Cons.prems
    by blast
  have sublist_connection: "pos_limit_branch = (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))#pos_limit_sublist"
    using Cons.prems(3) sublist_prop list_rec_prop(3)
    by simp 
  have list_prop: "map (λx. rat_of_int (Sturm_Tarski.sign (sgn_pos_inf x)))
     (map (eval_mpoly_poly val) (a#qs)) = 
  (rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val a)))) # map (λx. rat_of_int (Sturm_Tarski.sign (sgn_pos_inf x)))
     (map (eval_mpoly_poly val) qs)"
    by simp
  have tail_prop: "pos_limit_branch =
    (if r = 0 then 0
     else Sturm_Tarski.sign
           (lookup_assump (Polynomial.lead_coeff r) branch_assms)) #
      map (λx. rat_of_int (Sturm_Tarski.sign (sgn_pos_inf x)))
     (map (eval_mpoly_poly val) qs)"
    using sublist_connection ind_prop  unfolding sgn_pos_inf_rat_list_def
    by auto 
  have subs: "set new_assumps ⊆ set branch_assms"
    using deconstruct_prop list_rec_prop snd_elem_inset branch_init_assms_subset 
    by presburger
  then have r_sign: "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val a))) = 
     (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))"
    using pos_limit_point_on_branch_init deconstruct_prop(1) local.Cons(3) subsetD
    by (smt (verit, ccfv_threshold))
  have r_inv: "r = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i ∧ i ≠ 0))"
    using lc_assump_generation_inv
    by (meson deconstruct_prop(1)) 
  have r_match: " (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
  proof - 
    {assume *: "r = 0"
      then have "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
        by auto 
    } moreover {assume *: "r ≠ 0"
      then obtain i1 where i1_prop: "lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i1 ∧ i1 ≠ 0"
        using r_inv by auto 
      then obtain i2 where i2_prop: "lookup_assump_aux (Polynomial.lead_coeff r) branch_assms = Some i2 ∧ i2 ≠ 0"
        using lookup_assump_aux_subset_consistency subs
        using Cons.prems(2) by blast 
      then have " Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps) = 
      Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms)"
        using lookup_assump_aux_subset_consistent_sign subs
          i1_prop i2_prop Cons.prems(2)  
      proof -
        obtain mm :: "real list ⇒ (real mpoly × rat) list ⇒ real mpoly" and rr :: "real list ⇒ (real mpoly × rat) list ⇒ rat" where
          "∀x4 x5. (∃v6 v7. (v6, v7) ∈ set x5 ∧ ¬ satisfies_evaluation x4 v6 v7) = ((mm x4 x5, rr x4 x5) ∈ set x5 ∧ ¬ satisfies_evaluation x4 (mm x4 x5) (rr x4 x5))"
          by moura
        then have "∀ps rs psa p r ra. ((mm rs ps, rr rs ps) ∈ set ps ∧ ¬ satisfies_evaluation rs (mm rs ps) (rr rs ps) ∨ ¬ set psa ⊆ set ps ∨ lookup_assump_aux (Polynomial.lead_coeff p) psa ≠ Some r ∨ lookup_assump_aux (Polynomial.lead_coeff p) ps ≠ Some ra) ∨ (Sturm_Tarski.sign r) = Sturm_Tarski.sign ra"
          by (meson lookup_assump_aux_subset_consistent_sign)
        then have "(Sturm_Tarski.sign i1) = Sturm_Tarski.sign i2"
          using i1_prop i2_prop local.Cons(3) subs by blast
        then show ?thesis
          by (simp add: i1_prop i2_prop)
      qed
        (*  by (smt (verit, del_insts) lookup_assump.simps option.case(2)) *)
      then have "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
        by auto
    }
    ultimately show ?thesis
      by auto
  qed
  then have "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val a))) = 
     (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
    using r_sign r_match
    by fastforce 
  then have "pos_limit_branch = (rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val a)))) #
    (map (λx. rat_of_int (Sturm_Tarski.sign (sgn_pos_inf x)))
     (map (eval_mpoly_poly val) qs)) " 
    using tail_prop
    by (smt (verit, ccfv_threshold) list.inj_map_strong list.map(2) of_rat_hom.eq_iff) 
  then show ?case using  list_prop
    using sgn_pos_inf_rat_list_def 
    by (auto)
qed

lemma neg_limit_point_on_branch_init:
  assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
  assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
  shows "rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val init_q))) = 
     (if q = 0 then 0 else (Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))*(-1)^(Polynomial.degree q))"
proof - 
  have at_inf: "rat_of_int
     (Sturm_Tarski.sign  (sgn_class.sgn (Polynomial.lead_coeff (eval_mpoly_poly val init_q)))) =
    (if q = 0 then 0
     else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))"
    using assms  pos_limit_point_on_branch_init 
    unfolding sgn_pos_inf_def 
    by auto
  have "Polynomial.degree q = Polynomial.degree (eval_mpoly_poly val init_q)"
    using check_constant_degree_match assms by auto  
  then show ?thesis using at_inf
    unfolding sgn_neg_inf_def
    using Sturm_Tarski_casting degree_0 even_zero more_arith_simps(6) more_arith_simps(8) ring_1_class.minus_one_power_iff by auto
      (* Takes a couple seconds to load *)
qed

lemma neg_limit_point_on_branch_list:
  assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
  assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
  assumes "(pos_limit_branch, neg_limit_branch) = limit_points_on_branch (branch_assms, branch_poly_list)"
  shows "map rat_of_int (sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs)) = neg_limit_branch"
  using assms
proof (induct qs arbitrary: pos_limit_branch neg_limit_branch branch_assms branch_poly_list init_assumps)
  case Nil
  then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
    using lc_assump_generation_list.simps
    by auto
  then have "branch_poly_list = []"
    using in_set_member
    by simp 
  then show ?case using Nil.prems 
    unfolding eval_mpoly_poly_def sgn_neg_inf_rat_list_def
    by auto
next
  case (Cons a qs) 
  let ?rec = "lc_assump_generation a init_assumps"
  have inset: "(branch_assms,branch_poly_list) ∈ set (
    concat (map (
      λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
    using Cons.prems lc_assump_generation_list.simps
    by auto 
  then obtain new_assumps r where deconstruct_prop:
    "(new_assumps, r) ∈ set ?rec"
    "(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
      map (λelem. (fst elem, r#(snd elem))) list_rec)"
    using inset
    by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
  then obtain elem list_rec where list_rec_prop:
    "list_rec = lc_assump_generation_list qs new_assumps"
    "elem ∈ set list_rec"
    "(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))" 
    by auto
  then have snd_elem_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
    using deconstruct_prop by auto
  obtain pos_limit_sublist neg_limit_sublist where sublist_prop:
    "(pos_limit_sublist, neg_limit_sublist) = limit_points_on_branch (branch_assms, snd elem)"
    by auto 
  then have ind_prop_var: "neg_limit_sublist = map rat_of_int (sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs))"
    using snd_elem_inset Cons.hyps Cons.prems by blast
  then have ind_prop: "neg_limit_sublist = sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs)"
    by auto
  have sublist_connection: "pos_limit_branch = (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))#pos_limit_sublist"
    using Cons.prems(3) sublist_prop list_rec_prop(3)
    by simp 
  then have sublist_connection_var: "pos_limit_branch = (if r = 0 then 0 else (rat_of_int ∘ Sturm_Tarski.sign) (lookup_assump (Polynomial.lead_coeff r) branch_assms))#pos_limit_sublist"
    using Cons.prems(3) sublist_prop list_rec_prop(3)
    by simp 
  have list_prop: "map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
     (map (eval_mpoly_poly val) (a#qs)) = 
  (rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val a)))) # map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
     (map (eval_mpoly_poly val) qs)"
    by simp
  have ind_prop_var2: "neg_limit_sublist =
     (map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x))
       (map (eval_mpoly_poly val) qs))"
    using ind_prop_var unfolding sgn_neg_inf_rat_list_def 
    by auto
  have "neg_limit_branch =
    (if r = 0 then (0::rat)
     else ((rat_of_int ∘ Sturm_Tarski.sign)
           (lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r))) #
   map (λx. ((rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x)))
     (map (eval_mpoly_poly val) qs)"
    using  sublist_connection_var ind_prop_var2 local.Cons(4)  unfolding sgn_neg_inf_rat_list_def 
    unfolding limit_points_on_branch.simps
    by (metis (no_types, lifting) limit_points_on_branch.simps list.simps(9) list_rec_prop(3) prod.simps(1) sublist_prop)
  then have tail_prop_helper: "neg_limit_branch =
    (if r = 0 then 0
     else rat_of_int (Sturm_Tarski.sign
           (lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r))) #
   map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
     (map (eval_mpoly_poly val) qs)"
    by auto
  then have tail_prop: "neg_limit_branch =
    (if r = 0 then 0
     else Sturm_Tarski.sign
           (lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r)) #
      map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
     (map (eval_mpoly_poly val) qs)"
    by (smt (verit, ccfv_threshold) list.map(2) of_int_hom.hom_zero of_rat_of_int_eq)
  have subs: "set new_assumps ⊆ set branch_assms"
    using deconstruct_prop list_rec_prop snd_elem_inset branch_init_assms_subset 
    by presburger
  then have r_sign: "rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val a))) = 
     (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps)*(-1)^(Polynomial.degree r))"
    using neg_limit_point_on_branch_init deconstruct_prop(1) local.Cons(3) subsetD
    by (smt (verit, ccfv_threshold))
  have r_inv: "r = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i ∧ i ≠ 0))"
    using lc_assump_generation_inv
    by (meson deconstruct_prop(1)) 
  have r_match_pre: " (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
    =  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
  proof - 
    {assume *: "r = 0"
      then have "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
        =  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
        by auto 
    } moreover {assume *: "r ≠ 0"
      then obtain i1 where i1_prop: "lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i1 ∧ i1 ≠ 0"
        using r_inv by auto 
      then obtain i2 where i2_prop: "lookup_assump_aux (Polynomial.lead_coeff r) branch_assms = Some i2 ∧ i2 ≠ 0"
        using lookup_assump_aux_subset_consistency subs
        using Cons.prems(2) by blast 
      then have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps) = 
      Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms)"
        using lookup_assump_aux_subset_consistent_sign subs
          i1_prop i2_prop Cons.prems(2)
      proof -
        obtain mm :: "real list ⇒ (real mpoly × rat) list ⇒ real mpoly" and rr :: "real list ⇒ (real mpoly × rat) list ⇒ rat" where
          "∀x4 x5. (∃v6 v7. (v6, v7) ∈ set x5 ∧ ¬ satisfies_evaluation x4 v6 v7) = ((mm x4 x5, rr x4 x5) ∈ set x5 ∧ ¬ satisfies_evaluation x4 (mm x4 x5) (rr x4 x5))"
          by moura
        then have "∀ps rs psa p r ra. ((mm rs ps, rr rs ps) ∈ set ps ∧ ¬ satisfies_evaluation rs (mm rs ps) (rr rs ps) ∨ ¬ set psa ⊆ set ps ∨ lookup_assump_aux (Polynomial.lead_coeff p) psa ≠ Some r ∨ lookup_assump_aux (Polynomial.lead_coeff p) ps ≠ Some ra) ∨ (Sturm_Tarski.sign r) = Sturm_Tarski.sign ra"
          by (meson lookup_assump_aux_subset_consistent_sign)
        then have "(Sturm_Tarski.sign i1) = Sturm_Tarski.sign i2"
          using i1_prop i2_prop local.Cons(3) subs by blast
        then show ?thesis
          by (simp add: i1_prop i2_prop)
      qed
        (*  by (smt (verit, del_insts) lookup_assump.simps option.case(2)) *)
      then have "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
        =  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
        by auto
    }
    ultimately show ?thesis
      by auto
  qed
  then have r_match: "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps)*(-1)^(Polynomial.degree r))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r))"
    by metis
  then have "rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val a))) = 
     (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r))"
    using r_sign r_match
    by fastforce 
  then have "neg_limit_branch = (rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val a)))) #
    (map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
     (map (eval_mpoly_poly val) qs)) " 
    using tail_prop tail_prop_helper
    by (simp add: of_rat_hom.injectivity)
  then show ?case using  list_prop
    using sgn_neg_inf_rat_list_def
    by auto
qed

lemma complex_rat_casting_lemma:
  fixes a:: "int list"
  fixes b:: "rat list"
  shows "map complex_of_int a = map of_rat b ⟹ map rat_of_int a = b"
  by (metis (no_types, lifting) list.inj_map_strong list.map_comp of_rat_hom.injectivity of_rat_of_int)

lemma complex_rat_casting_lemma_sets:
  fixes a:: "rat list list"
  fixes b1:: "int list"
  fixes b2:: "int list"
  fixes c:: "rat list list"
  assumes "set (map (map of_rat) a) ∪ {map complex_of_int b1, map complex_of_int b2} 
    = set (map (map of_rat) c)"
  shows "set a ∪ {map rat_of_int b1, map rat_of_int b2} = set c"
proof - 
  have "map complex_of_int b1 ∈ set (map (map of_rat) c)"
    using assms by auto 
  then have h1: "map rat_of_int b1 ∈ set c"
    using complex_rat_casting_lemma by auto
  have "map complex_of_int b2 ∈ set (map (map of_rat) c)"
    using assms by auto 
  then have h2: "map rat_of_int b2 ∈ set c"
    using complex_rat_casting_lemma by auto
  have set_lem: "⋀ a b c . a ∪ b = c ⟹ a ⊆ c"
    by blast
  have "set (map (map of_rat) a) ⊆ set (map (map of_rat) c)"
    using assms set_lem[of "set (map (map of_rat) a)" "{map complex_of_int b1, map complex_of_int b2}" "set (map (map of_rat) c)"]
    by auto
  then have "⋀x. x ∈ set (map (map of_rat) a) ⟹ x ∈ set (map (map of_rat) c)"
    by auto 
  then have h3: "⋀x. x ∈ set a ⟹ x ∈ set c"
    using complex_rat_casting_lemma
    by fastforce 
  have h4_a: "⋀x. x ∈ set (map (map of_rat) c) ⟹
         x ≠ map complex_of_int b1 ⟹ x ∉ set (map (map of_rat) a) ⟹ x = map complex_of_int b2"
    using assms
    by blast 
  have h4: "⋀x. x ∈ set c ⟹
         x ≠ map rat_of_int b1 ⟹ x ∉ set a ⟹ x = map rat_of_int b2"
  proof - 
    fix x
    assume a1: "x ∈ set c"
    assume a2: "x ≠ map rat_of_int b1" 
    assume a3: "x ∉ set a"
    have "((map of_rat x)::complex list) ∈ set (map (map of_rat) c)"
      using a1 by auto 
    then have impl: "((map of_rat x)::complex list) ≠ map complex_of_int b1 ⟹ (map of_rat x) ∉ set (map (map of_rat) a) ⟹ (map of_rat x) = map complex_of_int b2"
      using h4_a[of "((map of_rat x)::complex list)"]
      using a3 imageE inj_map_eq_map list.set_map of_rat_hom.inj_f by fastforce 
    have impl_h1: "((map of_rat x)::complex list) ≠ map complex_of_int b1"
      using a2 complex_rat_casting_lemma
      by metis
    have impl_h2: "(map of_rat x) ∉ set (map (map of_rat) a)"
      using a3 complex_rat_casting_lemma by (auto) 
    then have "(map of_rat x) = map complex_of_int b2"
      using impl impl_h1 impl_h2 by auto 
    then show "x = map rat_of_int b2"
      using complex_rat_casting_lemma by metis 
  qed
  show ?thesis using h1 h2 h3 h4 by auto
qed

lemma complex_rat_casting_lemma_sets2:
  shows "{map rat_of_int
    (map (λx. Sturm_Tarski.sign (sgn_neg_inf x))
      (map (eval_mpoly_poly val) qs)),
   map rat_of_int
    (map (λx. Sturm_Tarski.sign (sgn_pos_inf x))
      (map (eval_mpoly_poly val) qs))} = {map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x))
      (map (eval_mpoly_poly val) qs),
     map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_pos_inf x))
      (map (eval_mpoly_poly val) qs)}"
proof - 
  have h1: "map rat_of_int
    (map (λx. Sturm_Tarski.sign (sgn_neg_inf x))
      (map (eval_mpoly_poly val) qs)) = map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x))
      (map (eval_mpoly_poly val) qs)"
    by auto
  have h2: "map rat_of_int
    (map (λx. Sturm_Tarski.sign (sgn_pos_inf x))
      (map (eval_mpoly_poly val) qs)) = map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_pos_inf x))
      (map (eval_mpoly_poly val) qs)"
    by auto
  show ?thesis using h1 h2
    by auto 
qed

lemma sign_determination_inner_gives_noncomp_signs_at_roots:
  assumes "(assumps, signs) ∈ set (sign_determination_inner qs init_assumps)"
  assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  shows "set signs = (consistent_sign_vectors_R (map (eval_mpoly_poly val) qs) UNIV)"
proof - 
  have elem_in_set: "(assumps, signs) ∈ set (let branches = lc_assump_generation_list qs init_assumps  in
    concat (map (λbranch. 
    let poly_p_branch = poly_p_in_branch branch;
        (pos_limit_branch, neg_limit_branch) = limit_points_on_branch branch;
        calculate_data_branch = extract_signs (calculate_data_assumps_M poly_p_branch (snd branch) (fst branch))
     in map (λ(a, signs). (a, pos_limit_branch#neg_limit_branch#signs)) calculate_data_branch
    ) branches))"
    using assms 
    by auto
  obtain branch where branch_prop: "branch ∈ set (lc_assump_generation_list qs init_assumps)"
    "(assumps, signs) ∈ set (
    let poly_p_branch = poly_p_in_branch branch;
        (pos_limit_branch, neg_limit_branch) = limit_points_on_branch branch;
        calculate_data_branch = extract_signs (calculate_data_assumps_M poly_p_branch (snd branch) (fst branch))
    in map (λ(a, signs). (a, pos_limit_branch#neg_limit_branch#signs)) calculate_data_branch)"
    using elem_in_set
    by auto
  then obtain branch_assms branch_poly_list where branch_is: 
    "branch = (branch_assms, branch_poly_list)"
    using poly_p_in_branch.cases by blast
  then obtain calculate_data_branch poly_p_branch pos_limit_branch neg_limit_branch
    where branch_prop_expanded:
      "poly_p_branch = poly_p_in_branch branch"
      "(pos_limit_branch, neg_limit_branch) = limit_points_on_branch branch"
      "calculate_data_branch = extract_signs (calculate_data_assumps_M poly_p_branch branch_poly_list branch_assms)"
      "branch ∈ set (lc_assump_generation_list qs init_assumps)"
      "(assumps, signs) ∈ set (
       map (λ(a, signs). (a, pos_limit_branch#neg_limit_branch#signs)) calculate_data_branch)"
    using branch_prop
    by (metis (no_types, lifting) case_prod_beta fst_conv prod.exhaust_sel snd_conv)
  obtain calc_a calc_signs where calc_prop:
    "(calc_a, calc_signs) ∈ set calculate_data_branch"
    "(assumps, signs) = (calc_a, pos_limit_branch#neg_limit_branch#calc_signs)"
    using in_set_member branch_prop_expanded(5)
    by auto
  then have branch_assms_subset: "set branch_assms ⊆ set assumps" 
    using branch_prop_expanded(3) extract_signs_M_subset
    by blast
  have "set init_assumps ⊆ set branch_assms"
    using branch_is branch_prop(1) branch_init_assms_subset
    by blast
  have assumps_calc_a: "assumps = calc_a"
    using calc_prop by auto 
  let ?poly_p_branch = "poly_p_in_branch (branch_assms, branch_poly_list)"
  have nonz_poly_p: "eval_mpoly_poly val ?poly_p_branch ≠ 0"
    using poly_p_nonzero_on_branch
    using ‹set branch_assms ⊆ set assumps› assms(2) branch_is branch_prop(1) by blast 
  have map_branch_poly_list: "(map (eval_mpoly_poly val) qs) = (map (eval_mpoly_poly val) branch_poly_list)"
    using map_branch_poly_list
    using assms(2) branch_assms_subset branch_is branch_prop(1) by blast 
  have "(calc_a, calc_signs)
    ∈ set (calculate_data_to_signs (calculate_data_assumps_M poly_p_branch branch_poly_list branch_assms))"
    using calc_prop branch_prop_expanded calc_data_to_signs_and_extract_signs
    by metis
  then have "(assumps, calc_signs)
    ∈ set (calculate_data_to_signs (calculate_data_assumps_M poly_p_branch branch_poly_list branch_assms))"
    using assumps_calc_a by auto  
  then have "set calc_signs = set(characterize_consistent_signs_at_roots (eval_mpoly_poly val ?poly_p_branch) (map (eval_mpoly_poly val) branch_poly_list))"
    using nonz_poly_p calculate_data_assumps_gives_noncomp_signs_at_roots[of assumps signs poly_p_branch branch_poly_list branch_assms val ]
    using assms(2) branch_is branch_prop_expanded(1) calculate_data_assumps_gives_noncomp_signs_at_roots by blast
  then have calc_signs_is: "set calc_signs = set(characterize_consistent_signs_at_roots (eval_mpoly_poly val ?poly_p_branch) (map (eval_mpoly_poly val) qs))"
    using map_branch_poly_list by auto
  have poly_p_is: "poly_p_in_branch (branch_assms, branch_poly_list) = (if (check_all_const_deg_gen branch_poly_list = True) then  [:0, 1:] else 
  (pderiv (prod_list_var_gen branch_poly_list)) * (prod_list_var_gen branch_poly_list))"
    by auto 
  have const_match: "(check_all_const_deg_gen branch_poly_list) = (check_all_const_deg_gen (map (eval_mpoly_poly val) qs))"
    using check_constant_degree_match_list
    using assms(2) branch_assms_subset branch_is branch_prop(1) by blast 
  have "eval_mpoly_poly val (prod_list_var_gen branch_poly_list) =
    prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)"
    using eval_prod_list_var_gen_match
    using assms(2) branch_assms_subset branch_is branch_prop(1) by blast
  then have same_prod:  "eval_mpoly_poly val ((pderiv (prod_list_var_gen branch_poly_list)) * (prod_list_var_gen branch_poly_list))
= pderiv (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)) * (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list))"
    by (metis eval_mpoly_poly_comm_ring_hom.hom_mult pderiv_commutes)
  {assume *: "check_all_const_deg_gen branch_poly_list = True"
    then have "?poly_p_branch = [: 0, 1 :]"
      using poly_p_is by presburger
    then have "(eval_mpoly_poly val ?poly_p_branch) = [:0, 1:]"
      unfolding eval_mpoly_poly_def
      by auto
    then have "(eval_mpoly_poly val ?poly_p_branch) =  (poly_f_nocrb (map (eval_mpoly_poly val) qs))"
      unfolding poly_f_nocrb_def using const_match check_all_const_deg_match "*" 
      by presburger
  } 
  moreover {assume *: "check_all_const_deg_gen branch_poly_list = False"
    then have "(eval_mpoly_poly val ?poly_p_branch)  = pderiv (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)) * (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list))"
      using poly_p_is same_prod by auto 
    then have h1: "(eval_mpoly_poly val ?poly_p_branch)  = pderiv (prod_list_var_gen (map (eval_mpoly_poly val) qs)) * (prod_list_var_gen (map (eval_mpoly_poly val) qs))"
      using map_branch_poly_list
      by presburger 
    have "(check_all_const_deg (map (eval_mpoly_poly val) qs) = False) "
      using * const_match check_all_const_deg_match by auto
    then have "(eval_mpoly_poly val ?poly_p_branch) =  (poly_f_nocrb (map (eval_mpoly_poly val) qs))"
      using h1 prod_list_var_match
      unfolding poly_f_nocrb_def
      by metis 
  }
  ultimately have poly_branch_no_crb_connect: "(eval_mpoly_poly val ?poly_p_branch) =  (poly_f_nocrb (map (eval_mpoly_poly val) qs))"
    by auto 
  let ?eval_qs = "(map (eval_mpoly_poly val) qs)"
  have "set calc_signs =
    set (characterize_consistent_signs_at_roots (poly_f_nocrb ?eval_qs) ?eval_qs)"
    using poly_branch_no_crb_connect calc_signs_is
    by presburger 
      (* Use Renegar_Modified *)
  then have calc_signs_relation: "(set calc_signs) ∪ {sgn_neg_inf_rat_list ?eval_qs, sgn_pos_inf_rat_list ?eval_qs} =
    set (characterize_consistent_signs_at_roots (poly_f ?eval_qs) ?eval_qs)"
    using poly_f_ncrb_connection[of ?eval_qs] 
    by auto
      (* Some minor casting details *)
  then have "set calc_signs ∪
    {map rat_of_int
      (sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs)),
     map rat_of_int
      (sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs))} =
    set (characterize_consistent_signs_at_roots
          (poly_f (map (eval_mpoly_poly val) qs))
          (map (eval_mpoly_poly val) qs))"
    unfolding sgn_neg_inf_rat_list2_def sgn_pos_inf_rat_list2_def 
    using complex_rat_casting_lemma_sets[of calc_signs "(sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs))" "(sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs))" 
        "(characterize_consistent_signs_at_roots (poly_f (map (eval_mpoly_poly val) qs)) (map (eval_mpoly_poly val) qs))"]  
    by (auto) 
  then have calc_signs_relation_var: "(set calc_signs) ∪ ({sgn_neg_inf_rat_list2 ?eval_qs, sgn_pos_inf_rat_list2 ?eval_qs}::rat list set) =
    set (characterize_consistent_signs_at_roots (poly_f ?eval_qs) ?eval_qs)"
    unfolding sgn_neg_inf_rat_list2_def sgn_pos_inf_rat_list2_def sgn_neg_inf_rat_list_def sgn_pos_inf_rat_list_def
    using complex_rat_casting_lemma_sets2
    by auto
  have pos_inf: "sgn_pos_inf_rat_list ?eval_qs = pos_limit_branch"
    using branch_prop_expanded(2) pos_limit_point_on_branch_list
    using assms(2) branch_assms_subset branch_is branch_prop(1)
    by (smt (verit, ccfv_threshold) basic_trans_rules(31) list.map_comp of_rat_of_int)
  then have pos_inf_var: "sgn_pos_inf_rat_list2 ?eval_qs = pos_limit_branch"
    unfolding sgn_pos_inf_rat_list2_def 
    using complex_rat_casting_lemma[of "(sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs))" pos_limit_branch]
    unfolding sgn_pos_inf_rat_list_def by auto
  have neg_inf: "sgn_neg_inf_rat_list ?eval_qs = neg_limit_branch"
    using branch_prop_expanded(2) neg_limit_point_on_branch_init
    using assms(2) branch_assms_subset branch_is branch_prop(1)
    by (smt (verit, ccfv_SIG) basic_trans_rules(31) list.map_comp neg_limit_point_on_branch_list of_rat_of_int)
  then have neg_inf_var: "sgn_neg_inf_rat_list2 ?eval_qs = neg_limit_branch"
    unfolding sgn_neg_inf_rat_list2_def 
    using complex_rat_casting_lemma[of "(sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs))" neg_limit_branch]
    unfolding sgn_neg_inf_rat_list_def 
    by auto 
  have "set signs = set (characterize_consistent_signs_at_roots (poly_f ?eval_qs) ?eval_qs)"
    using calc_signs_relation_var pos_inf_var neg_inf_var calc_prop(2)
    unfolding sgn_neg_inf_rat_list2_def sgn_pos_inf_rat_list2_def
    by auto
  then show "set signs = (consistent_sign_vectors_R (map (eval_mpoly_poly val) qs) UNIV)"
    using find_consistent_signs_at_roots_R poly_f_ncrb_connection calc_signs_is 
      main_step_R
    by (metis find_consistent_signs_R_def poly_f_nonzero) 
qed

subsection "Completeness"

(* This is the branch where all of the leading coefficients satisfy
the given sign conditions.  *)
lemma lc_assump_generation_valuation:
  assumes "⋀p n. (p,n) ∈ set init_assumps ⟹ satisfies_evaluation val p n"
  shows "∃branch ∈ set (lc_assump_generation q init_assumps).
      set (fst branch) ⊆ set (init_assumps) ∪ set
      (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
  using assms
proof (induct q init_assumps rule: lc_assump_generation_induct )
  case (Base q assumps)
  then show ?case 
    using lc_assump_generation.simps by auto
next
  case (Rec q assumps)
  let ?zero = "lc_assump_generation (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # assumps)"
  let ?one  = "((Polynomial.lead_coeff q, (1::rat)) # assumps, q)"
  let ?minus_one  = "((Polynomial.lead_coeff q, (-1::rat)) # assumps, q)"
  have set_is: "set (lc_assump_generation q assumps) = set (?one#?minus_one#?zero)"
    using Rec.hyps Rec(4) lc_assump_generation.simps by auto 
  let ?lc = "(Polynomial.lead_coeff q)"
  have eo: "satisfies_evaluation val ?lc (0::rat) ∨ satisfies_evaluation val ?lc (1::rat) ∨ satisfies_evaluation val ?lc (-1::rat)"
    unfolding satisfies_evaluation_def eval_mpoly_def Sturm_Tarski.sign_def by auto
  {assume *: "satisfies_evaluation val ?lc (1::rat) "
    then have "1 = mpoly_sign val (Polynomial.lead_coeff q)"
      unfolding satisfies_evaluation_def eval_mpoly_def mpoly_sign_def Sturm_Tarski.sign_def
      by simp
    then have "(Polynomial.lead_coeff q, 1)  ∈ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      by (simp add: Rec(1) coeff_in_coeffs)
    then have "set (fst ?one) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      by auto
    then have " ∃branch∈set (lc_assump_generation q assumps).
          set (fst branch) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      using set_is by auto
  } moreover
  {assume *: "satisfies_evaluation val ?lc (-1::rat) "
    then have "-1 = mpoly_sign val (Polynomial.lead_coeff q)"
      unfolding satisfies_evaluation_def eval_mpoly_def mpoly_sign_def Sturm_Tarski.sign_def
      by (smt (z3) of_int_1 of_int_minus rel_simps(66) zero_neq_neg_one)
    then have "(Polynomial.lead_coeff q, -1)  ∈ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      by (simp add: Rec(1) coeff_in_coeffs)
    then have "set (fst ?minus_one) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      by auto
    then have " ∃branch∈set (lc_assump_generation q assumps).
          set (fst branch) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      using set_is by auto
  } moreover {assume *: "satisfies_evaluation val ?lc (0::rat) "
    then have "∃branch∈set (lc_assump_generation (Multiv_Poly_Props.one_less_degree q) ((Polynomial.lead_coeff q, 0) # assumps)).
       set (fst branch)
       ⊆ set ((Polynomial.lead_coeff q, 0) # assumps) ∪
          set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)))"
      using lc_assump_generation.simps
      using Rec(3) Rec(4) by fastforce 
    then obtain branch where branch_prop: "branch∈set (lc_assump_generation (Multiv_Poly_Props.one_less_degree q) ((Polynomial.lead_coeff q, 0) # assumps))"
      "set (fst branch)
       ⊆ set ((Polynomial.lead_coeff q, 0) # assumps) ∪
          set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)))"
      by auto
    then have branch_prop_2: "branch∈set ?zero"
      by auto
    have "0 = mpoly_sign val (Polynomial.lead_coeff q)" using *
      unfolding satisfies_evaluation_def eval_mpoly_def mpoly_sign_def Sturm_Tarski.sign_def
      by simp
    then have lc_sign: "(Polynomial.lead_coeff q, 0) ∈ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      by (simp add: Rec(1) coeff_in_coeffs)
    {assume **: "Multiv_Poly_Props.one_less_degree q ≠ 0"
      then have "set (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)) ⊆ set (Polynomial.coeffs q)"
        using coeff_one_less_degree_subset unfolding Polynomial.coeffs_def
        by blast
      then have "set (fst branch) ⊆ set assumps ∪
          set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
        using branch_prop
        by (smt (verit, del_insts) UnCI UnE lc_sign imageE image_eqI list.set_map set_ConsD subset_code(1)) 
      then have "∃branch∈set (lc_assump_generation q assumps).
       set (fst branch)          
       ⊆ set assumps ∪
          set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
        using  branch_prop_2
        using set_is by force 
    }
    moreover {assume **: "Multiv_Poly_Props.one_less_degree q = 0"
      then have "∃branch∈set (lc_assump_generation q assumps).
         set (fst branch) ⊆ set assumps ∪
            set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
        using Rec.hyps(2) UnCI lc_sign insert_subset lc_assump_generation.elims list.set(2) option.case(1) prod.sel(1) subsetI
        by (metis (no_types, lifting))
    }
    ultimately have " ∃branch∈set (lc_assump_generation q assumps).
          set (fst branch) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      by auto
  }
  ultimately show ?case using eo by auto 
next
  case (Lookup0 q assumps)
  then obtain branch where branch_prop:"branch∈set (lc_assump_generation (Multiv_Poly_Props.one_less_degree q) assumps)"
    "set (fst branch)
       ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)))"
    by auto
  have same_gen: "lc_assump_generation (one_less_degree q) assumps = lc_assump_generation q assumps"
    using Lookup0.hyps lc_assump_generation.simps by auto
  then have branch_prop_2 :"branch∈set (lc_assump_generation q assumps)"
    using branch_prop(1) by auto
  {assume *: "Multiv_Poly_Props.one_less_degree q ≠ 0"
    then have "set (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)) ⊆ set (Polynomial.coeffs q)"
      using coeff_one_less_degree_subset unfolding Polynomial.coeffs_def
      by blast
    then have "set (fst branch)          
       ⊆ set assumps ∪
          set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      using branch_prop_2 branch_prop(2) by auto
    then have "∃branch∈set (lc_assump_generation q assumps).
       set (fst branch)          
       ⊆ set assumps ∪
          set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      using branch_prop_2
      by auto
  }
  moreover {assume *: "Multiv_Poly_Props.one_less_degree q = 0"
    then have "∃branch∈set (lc_assump_generation q assumps).
       set (fst branch)
       ⊆ set assumps ∪
          set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
      by (simp add: Lookup0(2) lc_assump_generation.simps)
  }
  ultimately show ?case 
    by force 
next
  case (LookupN0 q assumps r)
  then show ?case using lc_assump_generation.simps
    by simp 
qed

lemma lc_assump_generation_valuation_satisfies_eval:
  fixes q:: "rmpoly"
  assumes "(p,n) ∈ set (map (λx. (x, mpoly_sign val x)) ell)"
  shows "satisfies_evaluation val p n"
proof - 
  obtain c where c_prop: "c ∈ set ell"
    "(p, n) = (c, mpoly_sign val c)"
    using assms by auto
  have "satisfies_evaluation val c (mpoly_sign val c)"
    unfolding satisfies_evaluation_def mpoly_sign_def eval_mpoly_def
      Sturm_Tarski.sign_def by auto
  then show ?thesis
    using c_prop by auto
qed

(* relate lc_assump_generation_list to lc_assump_generation *)
lemma lc_assump_generation_list_valuation:
  assumes "⋀p n. (p,n) ∈ set init_assumps ⟹ satisfies_evaluation val p n"
  shows "∃branch ∈ set (lc_assump_generation_list qs init_assumps).
      set (fst branch) ⊆ set (init_assumps) ∪ set
      (map (λx. (x, mpoly_sign val x)) (coeffs_list qs))"
  using assms
proof (induct qs arbitrary: init_assumps)
  case Nil
  then show ?case 
    using lc_assump_generation_list.simps
    by simp 
next
  case (Cons a qs)
  then obtain branch_a where branch_a_prop: "branch_a ∈ set (lc_assump_generation a init_assumps)"
    "set (fst branch_a) ⊆ set (init_assumps) ∪ set
      (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs a))"
    using lc_assump_generation_valuation
    by blast 
  then obtain branch_a_assms branch_a_poly where branch_a_is: "branch_a = (branch_a_assms, branch_a_poly)"
    "set (branch_a_assms) ⊆ set (init_assumps) ∪ set
      (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs a))"
    by (meson prod.exhaust_sel)
  have inset: "set (map (λelem. (fst elem, branch_a_poly#(snd elem))) (lc_assump_generation_list qs branch_a_assms)) 
    ⊆ set (lc_assump_generation_list (a#qs) init_assumps)"
    using lc_assump_generation_list.simps branch_a_is(1) branch_a_prop(1)
    by auto
  have "⋀p n. (p,n) ∈ set branch_a_assms ⟹ satisfies_evaluation val p n"
    using lc_assump_generation_valuation_satisfies_eval branch_a_is(1) fst_conv local.Cons(2) Set.basic_monos(7) UnE
  proof -
    fix p :: "real mpoly" and n :: rat
    assume "(p, n) ∈ set branch_a_assms"
    then show "satisfies_evaluation val p n"
      by (meson UnE lc_assump_generation_valuation_satisfies_eval Set.basic_monos(7) branch_a_is(2) local.Cons(2))
  qed
  then obtain branch where branch_props:
    "branch∈set (lc_assump_generation_list qs branch_a_assms)"
    "set (fst branch)
       ⊆ set branch_a_assms ∪
          set (map (λx. (x, mpoly_sign val x)) (coeffs_list qs))"
    using Cons.hyps[of branch_a_assms] by auto
  then have branch_inset:
    "(fst branch, branch_a_poly#(snd branch))
    ∈ set (lc_assump_generation_list (a#qs) init_assumps)"
    using inset
    by auto
  then have subset_h: "set (fst branch) ⊆ set (init_assumps) ∪ (set
      (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs a))
    ∪ set (map (λx. (x, mpoly_sign val x)) (coeffs_list qs)))"
    using branch_props(2) branch_a_is(2) by auto
  have "coeffs_list (a # qs) = (Polynomial.coeffs a) @ (coeffs_list qs)"
    unfolding coeffs_list_def by auto
  then have same_set:
    "set (map (λx. (x, mpoly_sign val x)) (coeffs_list (a#qs))) = (set
      (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs a))
    ∪ set (map (λx. (x, mpoly_sign val x)) (coeffs_list qs)))"
    by auto
  then have "set (fst branch) ⊆ set (init_assumps) ∪ set
      (map (λx. (x, mpoly_sign val x)) (coeffs_list (a#qs)))"
    using subset_h by auto
  then show ?case
    using branch_inset
    by (metis (no_types, lifting) prod.sel(1))
qed

lemma base_case_info_M_assumps_complete:
  assumes "⋀p n. (p,n) ∈ set init_assumps ⟹ satisfies_evaluation val p n"
  shows  "∃ (assumps, mat_eq) ∈ set (base_case_info_M_assumps init_assumps).
   (∀ (p,n) ∈ set assumps. satisfies_evaluation val p n)"
  using assms unfolding base_case_info_M_assumps_def by auto

lemma matches_len_complete_spmods_ex:
  assumes "⋀p' n'. (p',n') ∈ set acc ⟹ satisfies_evaluation val p' n'"
  shows  "∃(assumps, sturm_seq) ∈ set (spmods_multiv p q acc).
    (∀ (p,n) ∈ set assumps. satisfies_evaluation val p n)"
  using assms
proof (induct p q acc rule: spmods_multiv_induct)
  case (Base p q acc)
  then show ?case 
    by (auto simp add: spmods_multiv.simps)
next
  case (Rec p q acc)
  let ?left = "spmods_multiv (one_less_degree p) q ((Polynomial.lead_coeff p, (0::rat)) # acc)"
  let ?res_one = "spmods_multiv_aux p q ((Polynomial.lead_coeff p, (1::rat)) # acc)"
  let ?res_minus_one = "spmods_multiv_aux p q ((Polynomial.lead_coeff p, (-1::rat)) # acc)"
  have spmods_is: "spmods_multiv p q acc = ?left @ (?res_one @ ?res_minus_one)"
    using spmods_multiv.simps Rec(1-2) by auto
  have "satisfies_evaluation val (Polynomial.lead_coeff p) 0 ∨
    satisfies_evaluation val (Polynomial.lead_coeff p) 1 ∨
    satisfies_evaluation val (Polynomial.lead_coeff p) (-1)"
    unfolding satisfies_evaluation_def
    apply auto
    using Sturm_Tarski.sign_cases
    by (metis of_int_1 of_int_minus) 
  then have q:"
  (∀p' n'. (p',n') ∈ set ((Polynomial.lead_coeff p, 0) # acc) ⟶ satisfies_evaluation val p' n') ∨
  (∀p' n'. (p',n') ∈ set ((Polynomial.lead_coeff p, 1) # acc) ⟶ satisfies_evaluation val p' n') ∨
  (∀p' n'. (p',n') ∈ set ((Polynomial.lead_coeff p, -1) # acc) ⟶ satisfies_evaluation val p' n')"
    using Rec 
    by simp 
  moreover {
    assume *:"(∀p' n'. (p',n') ∈ set ((Polynomial.lead_coeff p, 0) # acc) ⟶ satisfies_evaluation val p' n')"
    then have "∃a∈set (spmods_multiv (Multiv_Poly_Props.one_less_degree p) q
              ((Polynomial.lead_coeff p,