Theory Hybrid_Multiv_Matrix_Proofs

(* This file includes proofs for the multivariate 
  matrix equation construction from Hybrid_Multiv_Matrix.thy.
*)


theory Hybrid_Multiv_Matrix_Proofs
  imports
    "BenOr_Kozen_Reif.Matrix_Equation_Construction"
    Multiv_Tarski_Query
    "BenOr_Kozen_Reif.Renegar_Proofs"
    Hybrid_Multiv_Matrix
    Hybrid_Multiv_Algorithm
    Renegar_Modified

begin

hide_const "BKR_Decision.And"
hide_const "BKR_Decision.Or"

hide_const "UnivPoly.eval"

subsection "Connect multivariate Tarski queries to univariate"
lemma pull_out_pairs_length:
  shows "length (pull_out_pairs qs Is) = length Is"
  using pull_out_pairs.simps by force

lemma construct_NofI_M_subset_prop:
  assumes "(assumps, tq) ∈ set (construct_NofI_M p init_assumps qs1 qs2)"
  shows "set init_assumps ⊆ set assumps"
proof -
  have "(assumps, tq) ∈ set (map construct_NofI_single_M (construct_NofI_R_spmods p init_assumps qs1 qs2))"
    using assms
    by auto 
  then obtain mid_assumps tq_list where tuple_prop2: "(assumps, tq) = construct_NofI_single_M (mid_assumps, tq_list)"
    "(mid_assumps, tq_list) ∈ set (construct_NofI_R_spmods p init_assumps qs1 qs2)"
    by force
  have s1: "mid_assumps = assumps"
    using tuple_prop2(1)
    by simp 
  have s2: "set init_assumps ⊆ set mid_assumps"
    using tuple_prop2(2) spmods_multiv_assum_acc
    by (metis construct_NofI_R_spmods_def)
  then show "set init_assumps ⊆ set assumps"
    using s1 s2
    by blast 
qed

subsection "Connect multivariate RHS vector to univariate"

lemma construct_rhs_vector_rec_M_subset_prop_len1:
  assumes "(assumps, rhs_list) ∈ set (construct_rhs_vector_rec_M p init_assumps [a])"
  shows "set init_assumps ⊆ set assumps"
proof -
  obtain qs1 qs2 where a_prop: "a = (qs1, qs2)"
    using prod.exhaust by blast 
  have tuple_prop: "(assumps, rhs_list) ∈ set (map (λ(new_assumps, tq). (new_assumps, [tq])) (construct_NofI_M p init_assumps qs1 qs2))"
    using a_prop assms by auto
  then obtain tq where tq_prop: "rhs_list = [tq]"
    by auto
  let ?ell = "( map (λ(new_assumps, tq). (new_assumps, [tq])) (construct_NofI_M p init_assumps qs1 qs2))"
  have tuple_in_list: "(assumps, rhs_list) ∈ set ?ell"
    using tuple_prop 
    by auto
  then have "(assumps, tq) ∈ set (construct_NofI_M p init_assumps qs1 qs2)"  
    using tq_prop
    by (smt (verit, best) imageE list.inject list.set_map old.prod.case old.prod.simps(1) prod.collapse) 
  then have "(assumps, tq) ∈ set (construct_NofI_M p init_assumps qs1 qs2)"
    using tq_prop
    by metis 
  then have "(assumps, tq) ∈ set(map construct_NofI_single_M 
      (construct_NofI_R_spmods p init_assumps qs1 qs2))"
    by force
  then have "(assumps, tq) ∈ set (construct_NofI_M p init_assumps qs1 qs2)"
    using ‹(assumps, tq) ∈ set (construct_NofI_M p init_assumps qs1 qs2)› by force
  then show ?thesis using construct_NofI_M_subset_prop
    by blast
qed

lemma construct_rhs_vector_rec_M_subset_prop:
  assumes "(assumps, rhs_list) ∈ set (construct_rhs_vector_rec_M p init_assumps qs_list)"
  shows "set init_assumps ⊆ set assumps"
  using assms
proof (induct qs_list  arbitrary: assumps rhs_list init_assumps)
  case Nil
  then show ?case
    using construct_rhs_vector_rec_M.simps by auto
next
  case (Cons a qs_list)
  obtain qs1 qs2 where a_prop: "a = (qs1, qs2)"
    using Cons.prems Cons.hyps prod.exhaust
    by fastforce 
  { assume *: "qs_list = []"
    then have "set init_assumps ⊆ set assumps" using construct_rhs_vector_rec_M_subset_prop_len1 
        Cons.prems
      by blast 
  }
  moreover   { assume *: "length qs_list ≥ 1"
    then obtain v va where qs_list_prop: "qs_list = v # va"
      by (metis One_nat_def Suc_le_length_iff)
    let ?TQ_list = "construct_NofI_M p init_assumps qs1 qs2"
    have "(assumps, rhs_list) ∈ set (construct_rhs_vector_rec_M p init_assumps ((qs1, qs2)#qs_list))"
      using Cons.prems(1) * a_prop by auto
    then have "(assumps, rhs_list) ∈ set (concat ((map (λ(new_assumps, tq). 
    (let rec = construct_rhs_vector_rec_M p new_assumps qs_list in
     map (λr. (fst r,  tq#snd r)) rec)) ?TQ_list)))"
      using * a_prop qs_list_prop
      by (simp add: split_def) 
    then obtain new_assumps tq where tq_prop: "(new_assumps,tq) ∈ set (?TQ_list)"
      "(assumps, rhs_list) ∈ set (let rec = construct_rhs_vector_rec_M p new_assumps qs_list in
     map (λr. (fst r,  tq#snd r)) rec)"
      by auto
    then obtain rhs_rest where rhs_list_prop: "rhs_list = tq#rhs_rest"
      "(assumps, rhs_rest) ∈ set (construct_rhs_vector_rec_M p new_assumps qs_list)"
      by auto
    then have s1: "set new_assumps ⊆ set assumps"
      using Cons.hyps
      by auto 
    have s2: "set init_assumps ⊆ set new_assumps"
      using construct_NofI_M_subset_prop tq_prop(1) 
      by auto
    have "set init_assumps ⊆ set assumps"
      using s1 s2 
      by auto
  }
  ultimately  show ?case
    using Cons.prems
    by (metis length_0_conv less_one linorder_neqE_nat nat_less_le rel_simps(47)) 
qed

lemma construct_rhs_vector_rec_M_univariate:
  (* Intuitively, assumps really contains all of the assumptions that we care about *)
  assumes rhs_list_is: "(assumps, rhs_list) ∈ set(construct_rhs_vector_rec_M p init_assumps qs_list)"
  assumes val: "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  shows "rhs_list = map (λ(qs1,qs2).
    (construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1) (eval_mpoly_poly_list val qs2))) qs_list"
  using assms
proof (induct qs_list arbitrary: assumps rhs_list init_assumps)
  case Nil
  then show ?case 
    using construct_rhs_vector_rec_M.simps
    by auto
next
  case (Cons a qs_list)
  obtain qs1 qs2 where a_prop: "a = (qs1, qs2)"
    using Cons.prems Cons.hyps
    using prod.exhaust by blast 
  { assume *: "qs_list = []"
    let ?tq = "construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1) (eval_mpoly_poly_list val qs2)"
    have " (assumps, rhs_list) ∈ set (construct_rhs_vector_rec_M p init_assumps [(qs1, qs2)])"
      using Cons.prems(1) * a_prop by auto
    then have 
      "(assumps, rhs_list) ∈ set (let TQ_list = construct_NofI_M p init_assumps qs1 qs2 in
    map (λ(new_assumps, tq). (new_assumps, [tq])) TQ_list)"
      by (metis construct_rhs_vector_rec_M.simps(2))
    then have tuple_prop:
      "(assumps, rhs_list) ∈ set ( map (λ(new_assumps, tq). (new_assumps, [tq])) (construct_NofI_M p init_assumps qs1 qs2))"
      by auto
    then obtain tq where tq_prop: "rhs_list = [tq]"
      by auto
    let ?ell = "( map (λ(new_assumps, tq). (new_assumps, [tq])) (construct_NofI_M p init_assumps qs1 qs2))"
    have tuple_in_list: "(assumps, rhs_list) ∈ set ?ell"
      using tuple_prop
      by auto
    then have "(assumps, tq) ∈ set (construct_NofI_M p init_assumps qs1 qs2)"  
      using tq_prop
      by (smt (verit, best) imageE list.inject list.set_map old.prod.case old.prod.simps(1) prod.collapse) 
    then have "(assumps, tq) ∈ set (construct_NofI_M p init_assumps qs1 qs2)"
      using tq_prop
      by metis 
    then have "rhs_list = [construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1) (eval_mpoly_poly_list val qs2)]"
      using construct_NofI_M_univariate_tarski_query[of assumps tq p init_assumps qs1 qs2 val]
        Cons.prems(2) tq_prop
      by auto
    then have "rhs_list =
       map (λ(qs1, qs2).
               construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1)
                (eval_mpoly_poly_list val qs2))
        [(qs1, qs2)]"
      by auto
    then have "rhs_list =
       map (λ(qs1, qs2).
               construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1)
                (eval_mpoly_poly_list val qs2))
        (a # qs_list)"
      using * a_prop by auto
  }
  moreover {
    assume *: "qs_list ≠ []"
    then obtain v va where qs_list_prop: "qs_list = v # va"
      by (meson neq_Nil_conv)
    let ?tq = "construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1) (eval_mpoly_poly_list val qs2)"
    let ?TQ_list = "construct_NofI_M p init_assumps qs1 qs2"
    have "(assumps, rhs_list) ∈ set (construct_rhs_vector_rec_M p init_assumps ((qs1, qs2)#qs_list))"
      using Cons.prems(1) * a_prop by auto
    then have "(assumps, rhs_list) ∈ set (concat ((map (λ(new_assumps, tq). 
    (let rec = construct_rhs_vector_rec_M p new_assumps qs_list in
     map (λr. (fst r,  tq#snd r)) rec)) ?TQ_list)))"
      using * a_prop qs_list_prop
      by (simp add: split_def) 
    then obtain new_assumps tq where tq_prop: "(new_assumps,tq) ∈ set (?TQ_list)"
      "(assumps, rhs_list) ∈ set (let rec = construct_rhs_vector_rec_M p new_assumps qs_list in
     map (λr. (fst r,  tq#snd r)) rec)"
      by auto
    then obtain rhs_rest where rhs_list_prop: "rhs_list = tq#rhs_rest"
      "(assumps, rhs_rest) ∈ set (construct_rhs_vector_rec_M p new_assumps qs_list)"
      by auto
    then have subset: "set new_assumps ⊆ set assumps" using
        construct_rhs_vector_rec_M_subset_prop[of assumps rhs_rest p new_assumps qs_list]
      by auto 
    then have val_2: "⋀ p n. (p, n) ∈ set new_assumps ⟹ satisfies_evaluation val p n"
      using val
      by (meson Set.basic_monos(7) local.Cons(3)) 
    have tq_is: "tq = ?tq"
      using construct_NofI_M_univariate_tarski_query[of new_assumps tq p init_assumps qs1 qs2 val]
        tq_prop(1) Cons.prems(2) subset
      by blast
    have ih: "rhs_rest =
           map (λ(qs1, qs2).
                   construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1)
                    (eval_mpoly_poly_list val qs2))
            qs_list"
      using rhs_list_prop Cons.prems(2) val_2
      by (simp add: local.Cons(1))  
    then have "rhs_list =
       map (λ(qs1, qs2).
               construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1)
                (eval_mpoly_poly_list val qs2))
        (a # qs_list)"
      using a_prop tq_is ih rhs_list_prop
      by simp 
  }
  ultimately have "rhs_list =
       map (λ(qs1, qs2).
               construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1)
                (eval_mpoly_poly_list val qs2))
        (a # qs_list)"
    by blast
  then show ?case
    by blast 
qed

lemma retrieve_polys_prop:
  assumes "⋀x. x ∈ set ns ⟹ x < length qs"
  shows "(eval_mpoly_poly_list val (retrieve_polys qs ns)) = (retrieve_polys (map (eval_mpoly_poly val) qs) ns)"
  using assms unfolding eval_mpoly_poly_list_def retrieve_polys_def by auto

(* Intuitively, with the assumptions we have, we'll get a unique RHS vector
 i.e. the output of construct_NofI_M gives uniqueness (and matches the univariate
 case) *)
lemma construct_rhs_vector_M_univariate:
  (* Intuitively, assumps really contains all of the assumptions that we care about *)
  assumes rhs_vec_is: "(assumps, rhs_vec) ∈ set(construct_rhs_vector_M p init_assumps qs Is)"
  assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes well_def_subsets:  "⋀ Is1 Is2 n. (Is1, Is2) ∈ set Is ⟹ 
    (n ∈ set Is1 ∨ n ∈ set Is2) ⟹ n < length qs"
  shows "rhs_vec = construct_rhs_vector_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) Is"
proof  - 
  have "(assumps, rhs_vec) ∈ set (map (λres. (fst res, vec_of_list (snd res))) (construct_rhs_vector_rec_M p init_assumps (pull_out_pairs qs Is)))"
    using rhs_vec_is unfolding construct_rhs_vector_M_def by auto 
  then have "∃rhs_list. rhs_vec = vec_of_list rhs_list ∧ (assumps, rhs_list) ∈ set (map (λres. (fst res, snd res)) (construct_rhs_vector_rec_M p init_assumps (pull_out_pairs qs Is)))"
    by auto
  then obtain rhs_list where rhs_list_prop: "rhs_vec = vec_of_list rhs_list ∧ (assumps, rhs_list) ∈ set (map (λres. (fst res, snd res)) (construct_rhs_vector_rec_M p init_assumps (pull_out_pairs qs Is)))"
    by auto
  then have rhs_list_char: "rhs_list = map (λ(qs1,qs2).
    (construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val qs1) (eval_mpoly_poly_list val qs2))) (pull_out_pairs qs Is)"
    using assms construct_rhs_vector_rec_M_univariate
      (* Takes a couple seconds to load*)
    by (smt (verit, del_insts) case_prod_beta map_eq_conv map_idI prod.exhaust_sel)
  have lov_1: "list_of_vec (map_vec
     (λ(I1, I2).
         construct_NofI_R (eval_mpoly_poly val p) (retrieve_polys (map (eval_mpoly_poly val) qs) I1)
          (retrieve_polys (map (eval_mpoly_poly val) qs) I2))
     (vec_of_list Is)) = map (λ(I1, I2).
         construct_NofI_R (eval_mpoly_poly val p) (retrieve_polys (map (eval_mpoly_poly val) qs) I1)
          (retrieve_polys (map (eval_mpoly_poly val) qs) I2)) Is"
    by (metis list_vec vec_of_list_map)
  have lov_2: "list_of_vec rhs_vec = rhs_list"
    using rhs_list_prop
    using list_vec by blast 
  let ?rhs_list_var = "map (λ(I1, I2).
         construct_NofI_R (eval_mpoly_poly val p) (retrieve_polys (map (eval_mpoly_poly val) qs) I1)
          (retrieve_polys (map (eval_mpoly_poly val) qs) I2)) Is"
  have rhs_list_is: "rhs_list = ?rhs_list_var"
  proof - 
    have len_is1: "length (pull_out_pairs qs Is) = length Is"
      by simp
    then have "length rhs_list = length Is"
      using rhs_list_char
      by auto
    have len_is2: "length ?rhs_list_var = length Is"
      by auto
    have "⋀n. n  < length Is ⟹ rhs_list ! n = ?rhs_list_var ! n"
    proof - 
      fix n
      assume *: "n  < length Is"
      then obtain Is1 Is2 where Is_prop: "Is ! n = (Is1, Is2)"
        by fastforce
      then have "(pull_out_pairs qs Is) ! n = ((retrieve_polys qs Is1), (retrieve_polys qs Is2))"
        using "*" by force
      then have nth_1: "rhs_list ! n =  construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val (retrieve_polys qs Is1)) (eval_mpoly_poly_list val (retrieve_polys qs Is2))"     
        using rhs_list_char
        by (simp add: "*" len_is1) 
      have nth_2: "map (λ(I1, I2).
            construct_NofI_R (eval_mpoly_poly val p) (retrieve_polys (map (eval_mpoly_poly val) qs) I1)
             (retrieve_polys (map (eval_mpoly_poly val) qs) I2)) Is ! n
      = construct_NofI_R (eval_mpoly_poly val p) (retrieve_polys (map (eval_mpoly_poly val) qs) Is1)
             (retrieve_polys (map (eval_mpoly_poly val) qs) Is2)"
        using Is_prop
        by (simp add: "*")
      have ret_poly1: "(eval_mpoly_poly_list val (retrieve_polys qs Is1)) = (retrieve_polys (map (eval_mpoly_poly val) qs) Is1)"
        unfolding retrieve_polys_def eval_mpoly_poly_list_def 
        using well_def_subsets retrieve_polys_prop Is_prop       
        by (metis "*" eval_mpoly_poly_list_def in_set_conv_nth retrieve_polys_def)
      have ret_poly2: "(eval_mpoly_poly_list val (retrieve_polys qs Is2)) = (retrieve_polys (map (eval_mpoly_poly val) qs) Is2)"
        unfolding retrieve_polys_def eval_mpoly_poly_list_def 
        using well_def_subsets retrieve_polys_prop Is_prop
        by (metis "*" eval_mpoly_poly_list_def in_set_conv_nth retrieve_polys_def)
      have "construct_NofI_R (eval_mpoly_poly val p) (eval_mpoly_poly_list val (retrieve_polys qs Is1)) (eval_mpoly_poly_list val (retrieve_polys qs Is2))
        = construct_NofI_R (eval_mpoly_poly val p) (retrieve_polys (map (eval_mpoly_poly val) qs) Is1)
             (retrieve_polys (map (eval_mpoly_poly val) qs) Is2)"
        using ret_poly1 ret_poly2 
        by auto
      then show "rhs_list ! n = ?rhs_list_var ! n"
        using nth_1 nth_2 by auto 
    qed
    then show ?thesis
      using len_is1 len_is2
      by (metis ‹length rhs_list = length Is› nth_equalityI)
  qed
  then show ?thesis
    using rhs_list_is lov_2 lov_1
    unfolding construct_rhs_vector_R_def
    using rhs_list_prop by force 
qed

subsection "Connect multivariate LHS vector to univariate"

lemma solve_for_lhs_vector_M_univariate:
  assumes lhs_in: "(assumps, lhs_vec) ∈ set (solve_for_lhs_M p init_assumps qs subsets matr)"
  assumes val: "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes well_def_subsets:  "⋀ Is1 Is2 n. (Is1, Is2) ∈ set subsets ⟹ 
    (n ∈ set Is1 ∨ n ∈ set Is2) ⟹ n < length qs"
  shows "lhs_vec = solve_for_lhs_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) subsets matr"
proof - 
  let ?lhs_univ = "solve_for_lhs_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) subsets matr"
  have "(assumps, lhs_vec) ∈ set(map (λrhs. (fst rhs, solve_for_lhs_single_M p qs subsets matr (snd rhs))) (construct_rhs_vector_M p init_assumps qs subsets))"
    using lhs_in
    using solve_for_lhs_M_def by auto 
  then obtain rhs where rhs_prop: "rhs ∈ set(construct_rhs_vector_M p init_assumps qs subsets)"
    "(assumps, lhs_vec) = (fst rhs, solve_for_lhs_single_M p qs subsets matr (snd rhs))"
    by auto
  then have snd_is: "snd rhs = construct_rhs_vector_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) subsets"
    using construct_rhs_vector_M_univariate
    by (metis assms(2) fst_conv prod.collapse well_def_subsets)  
  have "fst rhs = assumps" using rhs_prop
    by force 
  have "?lhs_univ = mult_mat_vec (matr_option (dim_row matr) (mat_inverse_var matr)) (snd rhs)"
    using snd_is
    by (simp add: solve_for_lhs_R_def) 
  then show ?thesis
    using rhs_prop(2) unfolding solve_for_lhs_single_M_def 
    by auto
qed

subsection "Connect multivariate reduction step to univariate"

lemma reduce_system_single_M_univariate:
  assumes inset: "(assumps, mat_eq) ∈ set(reduce_system_single_M p qs (init_assumps, init_mat_eq))"
  assumes val: "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes init: "init_mat_eq = (m, (subs, signs))"
  assumes well_def_subsets:  "⋀ Is1 Is2 n. (Is1, Is2) ∈ set subs ⟹ 
    (n ∈ set Is1 ∨ n ∈ set Is2) ⟹ n < length qs"
  shows "mat_eq = reduce_system_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) qs), init_mat_eq)"
proof - 
  have "(assumps, mat_eq) ∈ set (map (λlhs. (fst lhs, reduction_step_R m signs subs (snd lhs))) (solve_for_lhs_M p init_assumps qs subs m))"
    using inset
    using assms(3)
    by force
  then obtain lhs where lhs_prop: "lhs ∈ set (solve_for_lhs_M p init_assumps qs subs m)"
    "(assumps, mat_eq) = (fst lhs, reduction_step_R m signs subs (snd lhs))"
    by auto
  then have "snd lhs = solve_for_lhs_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) subs m"
    using solve_for_lhs_vector_M_univariate assms
    by (smt (verit, best) prod.exhaust_sel prod.simps(1))
  then have "mat_eq = reduction_step_R m signs subs (solve_for_lhs_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) subs m)"
    using lhs_prop
    by force 
  then show ?thesis 
    using init
    using reduce_system_R.simps by presburger 
qed

lemma reduce_system_M_univariate:
  assumes "(assumps, mat_eq) ∈ set(reduce_system_M p qs input_list)"
  assumes val: "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes val_qs: "val_qs = (map (eval_mpoly_poly val) qs)"
  assumes all_subsets_well_def:  "⋀ init_assumps init_mat_eq Is1 Is2 n subs m signs. 
   (init_assumps, (m, (subs, signs))) ∈ set input_list ⟹
   (Is1, Is2) ∈ set subs ⟹ (n ∈ set Is1 ∨ n ∈ set Is2) ⟹ n < length qs"
  obtains acc mss where
    "(acc,mss) ∈ set (input_list)" 
    "mat_eq = reduce_system_R (eval_mpoly_poly val p) (val_qs,mss)"
proof -
  have "(assumps, mat_eq) ∈ set(concat (map (reduce_system_single_M p qs) input_list))"
    by (metis assms(1) reduce_system_M.simps)
  then obtain init_assumps init_m init_subs init_signs where
    mat_eq_prop: 
    "(init_assumps, (init_m, (init_subs, init_signs))) ∈ set input_list"
    "(assumps, mat_eq) ∈ set (reduce_system_single_M p qs (init_assumps, (init_m, (init_subs, init_signs))))"
    by auto
  then have well_def_subsets:  "⋀ Is1 Is2 n. (Is1, Is2) ∈ set init_subs ⟹ 
    (n ∈ set Is1 ∨ n ∈ set Is2) ⟹ n < length qs"
    using all_subsets_well_def
    by blast
  then have mat_eq_is: "mat_eq = reduce_system_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) qs), (init_m, (init_subs, init_signs)))"
    using reduce_system_single_M_univariate mat_eq_prop assms(2) by blast 
  then show ?thesis using mat_eq_prop
    using assms(3) that by blast
qed

lemma base_case_info_M_well_def:
  assumes "(init_assumps, (m, (subs, signs))) ∈ set base_case_info_M"
  assumes "(Is1, Is2) ∈ set subs"
  assumes "n ∈ set Is1 ∨ n ∈ set Is2"
  shows "n < 1"
proof -
  have "(m, (subs, signs)) = base_case_info_R" using assms(1)
    unfolding base_case_info_M_def using Renegar_Algorithm.base_case_info_R_def Renegar_Algorithm.base_case_info_R_def
    by simp
  then have s: "subs = [([], []),([0], []),([], [0])]" unfolding base_case_info_R_def
    by auto
  have "(n ∈ set Is1 ∨ n ∈ set Is2)" using assms(3)
    by (simp add: in_set_member)
  thus ?thesis using assms(2) unfolding s by auto
qed

subsection "Connect multivariate combining systems to univariate"

(* Well-definedness property to satisfy induction hypothesis *)
lemma base_case_with_assumps_info_M_well_def:
  assumes "(init_assumps, (m, (subs, signs))) ∈ set (base_case_info_M_assumps a)"
  assumes "(Is1, Is2) ∈ set subs"
  assumes "n ∈ set Is1 ∨ n ∈ set Is2"
  shows "n < 1"
proof -
  have "(m, (subs, signs)) = base_case_info_R" using assms(1)
    unfolding base_case_info_M_assumps_def 
    using Renegar_Algorithm.base_case_info_R_def Renegar_Algorithm.base_case_info_R_def
    by auto
  then have s: "subs = [([], []),([0], []),([], [0])]" unfolding base_case_info_R_def
    by auto
  have "(n ∈ set Is1 ∨ n ∈ set Is2)" using assms(3)
    by (simp add: in_set_member)
  thus ?thesis using assms(2) unfolding s by auto
qed

lemma concat_map_in_set:
  assumes "x ∈ set (concat (map f ls))"
  shows "∃i < length ls. x ∈ set (f (ls ! i))"
  using assms
  by (smt (verit, best) in_set_conv_nth length_map map_nth_eq_conv nth_concat_split) 

lemma combine_systems_R_snd:
  assumes "length qs1 = length new_qs1"
  shows "snd (combine_systems_R p (qs1, sys1) (qs2, sys2)) = 
    snd (combine_systems_R new_p (new_qs1, sys1) (new_qs2, sys2))"
proof - 
  obtain  m1 sub1 sgn1 where sys1: "sys1 = (m1, sub1, sgn1)"
    using prod_cases3 by blast
  obtain  m2 sub2 sgn2 where sys2: "sys2 = (m2, sub2, sgn2)"
    using prod_cases3 by blast 
  have h1: "snd (combine_systems_R p (qs1, sys1) (qs2, sys2)) = 
    snd (smash_systems_R p qs1 qs2 sub1 sub2 sgn1 sgn2 m1 m2)"
    using sys1 sys2 by auto 
  have h2: "snd (combine_systems_R new_p (new_qs1, sys1) (new_qs2, sys2)) = 
    snd (smash_systems_R new_p new_qs1 new_qs2 sub1 sub2 sgn1 sgn2 m1 m2)"
    using sys1 sys2 by auto 
  show ?thesis
    using h1 h2 assms unfolding smash_systems_R_def by auto
qed

subsection "Subset Properties"

lemma construct_rhs_vector_M_subset_prop:
  assumes "(assumps, rhs_vec) ∈ set (construct_rhs_vector_M p init_assumps qs subsets)"
  shows "set init_assumps ⊆ set assumps"
proof - 
  obtain rhs_list where "(assumps, rhs_list) ∈ set  (construct_rhs_vector_rec_M p init_assumps (pull_out_pairs qs subsets))" 
    "rhs_vec = vec_of_list rhs_list"
    using assms unfolding construct_rhs_vector_M_def by auto
  then show ?thesis
    using construct_rhs_vector_rec_M_subset_prop by auto
qed

lemma construct_lhs_vector_rec_M_subset_prop:
  assumes "(assumps, lhs_list) ∈ set (solve_for_lhs_M p init_assumps qs subsets matr)"
  shows "set init_assumps ⊆ set assumps"
proof - 
  obtain rhs_vec where "(assumps, rhs_vec) ∈ set (construct_rhs_vector_M p init_assumps qs subsets)" 
    "lhs_list = matr_option (dim_row matr) (mat_inverse_var matr) *⇩v rhs_vec "
    using assms unfolding solve_for_lhs_M_def solve_for_lhs_single_M_def 
    by auto 
  then show ?thesis
    using construct_rhs_vector_M_subset_prop[of assumps] by auto
qed

lemma reduce_system_single_M_subset_prop:
  assumes "(assumps, mat_eq) ∈ set (reduce_system_single_M p qs (init_assumps, (m,subs,signs)))"
  shows "set init_assumps ⊆ set assumps"
proof - 
  obtain lhs_vec where "(assumps, lhs_vec) ∈ set (solve_for_lhs_M p init_assumps qs subs m)" 
    "mat_eq = reduction_step_R m signs subs lhs_vec"
    using assms 
    by (auto) 
  then show ?thesis
    using construct_lhs_vector_rec_M_subset_prop[of assumps] 
    by auto
qed


lemma calculate_data_assumps_M_subset:
  assumes "(assumps, mat_eq) ∈ set (calculate_data_assumps_M p qs init_assumps)"
  shows "set init_assumps ⊆ set assumps"
  using assms
proof (induction "length qs" arbitrary: qs assumps mat_eq rule: less_induct)
  case less
  {assume *: "length qs = 0"
    then have "(assumps, mat_eq) ∈ set (map (λ(assumps,(a,(b,c))). (assumps, (a,b,map (drop 1) c))) (reduce_system_M p [1] (base_case_info_M_assumps init_assumps)))"
      using less.prems by auto 
    then obtain a b c where "(assumps, (a, (b, c))) ∈ set (reduce_system_M p [1] (base_case_info_M_assumps init_assumps))"
      by auto 
    then have "(assumps, (a, (b, c))) ∈ set (concat (map (reduce_system_single_M p [1]) [(init_assumps, base_case_info_R)]))"
      unfolding base_case_info_M_assumps_def
      using Renegar_Algorithm.base_case_info_R_def Renegar_Algorithm.base_case_info_R_def 
      by (auto) 
    then have "(assumps, (a, (b, c))) ∈ set( reduce_system_single_M p [1] (init_assumps, base_case_info_R))"
      by auto
    then have "set init_assumps ⊆ set assumps"
      unfolding base_case_info_R_def
      using reduce_system_single_M_subset_prop[of assumps "(a, (b, c))" p "[1]" init_assumps]
      by auto
  }
  moreover {assume *: "length qs = 1"
    then have "(assumps, mat_eq) ∈ set (reduce_system_M p qs (base_case_info_M_assumps init_assumps))"
      using less.prems by auto 
    then obtain a b c where "(assumps, (a, (b, c))) ∈ set (reduce_system_M p qs (base_case_info_M_assumps init_assumps))"
      by (smt (verit) prod.sel(2) prod_cases4)
    then have "(assumps, (a, (b, c))) ∈ set (concat (map (reduce_system_single_M p qs) [(init_assumps, base_case_info_R)]))"
      unfolding base_case_info_M_assumps_def 
      using Renegar_Algorithm.base_case_info_R_def Renegar_Algorithm.base_case_info_R_def 
      by (auto)
    then have "(assumps, (a, (b, c))) ∈ set( reduce_system_single_M p qs (init_assumps, base_case_info_R))"
      by auto
    then have "set init_assumps ⊆ set assumps"
      unfolding base_case_info_R_def
      using reduce_system_single_M_subset_prop[of assumps "(a, (b, c))" p qs init_assumps]
      by auto
  }
  moreover {assume *: "length qs > 1"
    let ?len = "length qs"
    let ?q1 = "take (?len div 2) qs"
    let ?left = "calculate_data_assumps_M p ?q1 init_assumps"
    let ?q2 = "drop (?len div 2) qs"
    let ?right = "calculate_data_assumps_M p ?q2 init_assumps"
    let ?comb = "combine_systems_M p ?q1 ?left ?q2 ?right"
    have len_q1_less: "length ?q1 < length qs"
      using * by auto
    have inset_red: "(assumps, mat_eq) ∈ set(reduce_system_M p (fst ?comb) (snd ?comb))"
      using * less.prems
      by (smt (verit, best) calculate_data_assumps_M.simps less_one nat_less_le not_one_less_zero)
    have "fst ?comb = qs"
      by auto
    then have "(assumps, mat_eq) ∈ set(reduce_system_M p qs (snd ?comb))"
      using inset_red 
      by auto
    then obtain assm_pre m_pre subs_pre signs_pre where assumps_reduce:
      "(assm_pre, (m_pre, subs_pre, signs_pre)) ∈ set (snd ?comb)"
      "(assumps, mat_eq) ∈ set(reduce_system_single_M p qs (assm_pre, (m_pre, subs_pre, signs_pre)))"
      by (metis concat_map_in_set find_consistent_signs_at_roots_single_M.cases nth_mem reduce_system_M.simps)
    then obtain meq1 meq2 assm1 assm2 where subsystems:
      "(assm1, meq1) ∈ set (calculate_data_assumps_M p ?q1 init_assumps)"
      "(assm2, meq2) ∈ set (calculate_data_assumps_M p ?q2 init_assumps)"
      "(assm_pre, (m_pre, subs_pre, signs_pre)) = combine_systems_single_M p ?q1 (assm1, meq1) ?q2 (assm2, meq2)"
      by auto (* Takes a second to load *)
    then have assm_pre: "assm_pre = assm1@assm2" 
      by auto
    have "set init_assumps ⊆ set assm1"
      using less.hyps[of ?q1] less.prems subsystems(1) len_q1_less
      by auto (* Takes a second to load *)
    then have "set init_assumps ⊆ set assm_pre" 
      using assm_pre by auto 
    then have "set init_assumps ⊆ set assumps"
      using assumps_reduce(2) reduce_system_single_M_subset_prop[of assumps mat_eq p qs assm_pre m_pre subs_pre signs_pre]
      by auto
  }
  ultimately show ?case
    by (meson less_one linorder_neqE_nat)
qed

lemma extract_signs_M_subset:
  assumes "(assumps, signs) ∈ set (extract_signs (calculate_data_assumps_M p qs init_assumps))"
  shows "set init_assumps ⊆ set assumps"
proof - 
  obtain mat_eq where 
    "(assumps, mat_eq) ∈ set (calculate_data_assumps_M p qs init_assumps)"
    "signs = snd (snd mat_eq)"
    using assms by auto
  then show ?thesis 
    using calculate_data_assumps_M_subset[of assumps mat_eq p qs init_assumps]
    by auto
qed

subsection "Top-level Results: Connect calculate data methods to univariate"

(* Well-definedness property to satisfy induction hypothesis *)
lemma all_list_constr_R_matches_well_def:
  assumes welldef: "all_list_constr_R subs (length q)"
  shows "(Is1, Is2) ∈ set (subs) ⟹ n ∈ set Is1 ∨ n ∈ set Is2 ⟹ n < length q"
proof -
  assume inset: "(Is1, Is2) ∈ set (subs)"
  assume inlist: "n ∈ set Is1 ∨ n ∈ set Is2"
  have welldef_var: "∀x. x ∈ set subs ⟶
        list_constr (fst x) (length q) ∧ list_constr (snd x) (length q)"
    using welldef  unfolding all_list_constr_R_def
    by (simp add: in_set_member)
  have "(Is1, Is2) ∈ set subs"
    using inset by auto 
  then have "(∀x∈set Is1. x < length q) ∧ (∀x∈set Is2. x < length q)"
    using welldef_var
    by (simp add: Ball_set list_constr_def)
  then show "n < length q"
    using inlist
    by metis
qed

lemma calculate_data_M_univariate:
  assumes mat_eq: "(assumps, mat_eq) ∈ set (calculate_data_M p qs)"
  assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes p_nonzero: "eval_mpoly_poly val p ≠ 0"
  shows "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) = mat_eq"
  using assms
proof (induct "length qs" arbitrary: val p mat_eq assumps qs rule: less_induct)
  case (less qs val p mat_eq assumps) 
  have "length qs = 0 ∨ length qs = 1 ∨ length qs > 1"
    by (meson less_one nat_neq_iff)
  moreover {assume *: "length qs = 0"
    let ?m = "(mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]])"
    let ?subs = "[([], []),([0], []),([], [0])]"
    let ?signs = "[[1],[0],[-1]]"
    let ?eval_p = "eval_mpoly_poly val p"
    have mat_eq_in: "(assumps, mat_eq) ∈ set (calculate_data_M p [])"
      using * less.prems(1) by auto 
    let ?map_base = "map (λ(assumps,(a,(b,c))). (assumps, (a,b,map (drop 1) c))) (reduce_system_M p [1] base_case_info_M)"
    have "(assumps, mat_eq) ∈ set ?map_base"
      using mat_eq_in 
      by auto
    then obtain a1 b1 c1 where a1b1c1_prop:
      "(assumps, (a1, (b1, c1))) ∈ set (reduce_system_M p [1] base_case_info_M)"
      "mat_eq = (a1, (b1, map (drop 1) c1))"
      by auto
    have base_case_well_def: "⋀init_assumps init_mat_eq Is1 Is2 n subs m signs.
        (init_assumps, m, subs, signs) ∈ set base_case_info_M ⟹
        (Is1, Is2) ∈ set subs ⟹ n ∈ set Is1 ∨ n ∈ set Is2 ⟹ n < length [1]"
      using base_case_info_M_well_def by auto
    have map_is: "[1] = map (eval_mpoly_poly val) [1] "
      unfolding eval_mpoly_poly_def eval_mpoly_def 
      by auto
   then have "∃acc mss. (acc,mss) ∈ set (base_case_info_M) ∧ (a1, (b1, c1)) = reduce_system_R (eval_mpoly_poly val p) ([1],mss)"
      using reduce_system_M_univariate[of "assumps" "(a1, b1, c1)" p "[1]" base_case_info_M val "[1]"]
        a1b1c1_prop less(3) base_case_well_def
      apply (auto) 
      by metis
    then obtain acc mss where a1b1c1_connect:
      "(acc,mss) ∈ set (base_case_info_M)" 
      "(a1, (b1, c1)) = reduce_system_R (eval_mpoly_poly val p) ([1],mss)"
      by auto
    then have mss_is: "mss = base_case_info_R"
      unfolding base_case_info_M_def 
      by auto
    obtain a b c where abc_prop: "(a, b, c) = reduction_step_R ?m ?signs ?subs (solve_for_lhs_R ?eval_p [1] ?subs ?m)"
      by (metis reduction_step_R.simps)
    then have "(a, b, c) = (a1, b1, c1)"
      using abc_prop a1b1c1_prop
      by (metis a1b1c1_connect(2) base_case_info_R_def mss_is reduce_system_R.simps) 
    then have mat_eq_is: "(a, b, map (drop (Suc 0)) c) = mat_eq"
      using a1b1c1_prop(2) by (auto) 
    have "qs = [] ⟹ mat_eq = (a, b, map (drop (Suc 0)) c) ⟹
      (case reduce_system_R (eval_mpoly_poly val p) ([1], base_case_info_R) of
      (a, b, c) ⇒ (a, b, map (drop (Suc 0)) c)) = (a, b, map (drop (Suc 0)) c) "
      using abc_prop unfolding base_case_info_R_def
      using  old.prod.case reduce_system_R.simps
      by (smt (verit, ccfv_SIG))
    then have "calculate_data_R ?eval_p (map (eval_mpoly_poly val) qs)= mat_eq"
      using * mat_eq_is
      by simp 
  }
  moreover {assume *: "length qs = 1"
    have meq: "(assumps, mat_eq) ∈ set (reduce_system_M p qs base_case_info_M)"
      using "*" le_eq_less_or_eq less(2) one_neq_zero by auto
    have **: "⋀init_assumps init_mat_eq Is1 Is2 n subs m signs.
      (init_assumps, m, subs, signs) ∈ set base_case_info_M ⟹
      (Is1, Is2) ∈ set subs ⟹
      n ∈ set Is1 ∨ n ∈ set Is2 ⟹
      n < length qs" unfolding *
      using base_case_info_M_well_def
      by meson
    from reduce_system_M_univariate[OF meq less(3), of " map (eval_mpoly_poly val)
   qs"]
    obtain acc mss where ams: "(acc,mss) ∈ set base_case_info_M" 
      "mat_eq = reduce_system_R (eval_mpoly_poly val p)
      (map (eval_mpoly_poly val) qs, mss)"
      using "**" by blast
    then have "mss = base_case_info_R" unfolding base_case_info_M_def 
      by auto
    then have "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) = mat_eq"
      using ams * by simp
  }
    (* Inductive case: progress by breaking down, using IH, then piecing back together.
      It's the reduction of a combination of two smaller matrix equation pieces. *)
  moreover {assume *: "length qs  > 1"
    have inset: "(assumps, mat_eq) ∈ set (calculate_data_M p qs)"
      using less.prems(1) by auto 
    let ?len = "length qs"
    let ?q1 = "take (?len div 2) qs"
    let ?q2 = "drop (?len div 2) qs"
    let ?left = "calculate_data_M p ?q1"
    let ?right = "calculate_data_M p ?q2"
    let ?comb = "combine_systems_M p ?q1 ?left ?q2 ?right"
    let ?eval_p = "(eval_mpoly_poly val p)"
    let ?eval_q1 = "(map (eval_mpoly_poly val) ?q1)"
    let ?eval_q2 = "(map (eval_mpoly_poly val) ?q2)"
    have map_q1: "map (eval_mpoly_poly val) ?q1 = 
      (take (length (map (eval_mpoly_poly val) qs) div 2) (map (eval_mpoly_poly val) qs))"
      by (auto simp add: take_map) 
    have map_q2: "map (eval_mpoly_poly val) ?q2 = 
      (drop (length (map (eval_mpoly_poly val) qs) div 2) (map (eval_mpoly_poly val) qs))"
      by (auto simp add: drop_map) 
    have "fst ?comb = qs" 
      by auto
    then have "(assumps, mat_eq) ∈ set (reduce_system_M p qs (snd ?comb))"
      using inset *
      by (smt (verit) calculate_data_M.simps less_numeral_extra(2) less_one nat_less_le)
    then have "(assumps, mat_eq) ∈ set (concat (map (reduce_system_single_M p qs) (snd ?comb)))"
      by (metis reduce_system_M.simps)
    then have "∃sys. sys ∈ set (snd ?comb) ∧ (assumps, mat_eq) ∈ set(reduce_system_single_M p qs sys)"
      using concat_map_in_set in_set_member
      by (metis nth_mem) 
    then obtain a_pre me_pre  where reduce_prop: "(a_pre, me_pre) ∈ set (snd ?comb)"
      "(assumps, mat_eq) ∈ set(reduce_system_single_M p qs (a_pre, me_pre))"
      by fastforce 
    then obtain a1 me1 a2 me2 where mes_prop: "(a1, me1) ∈ set ?left"
      "(a2, me2) ∈ set ?right"
      "(a_pre, me_pre) = combine_systems_single_M p ?q1 (a1, me1) ?q2 (a2, me2)"
      by auto
    then have a_pre: "a_pre = a1@a2" 
      by auto 
    have lengt: "length qs div 2 ≥ 1"
      using * by auto
    then have len_q1: "length ?q1 < length qs"
      by auto
    have len_q2: "length ?q2 < length qs"
      using lengt by auto
    obtain mat_pre subs_pre signs_pre where me_decomp:
      "me_pre = (mat_pre,subs_pre,signs_pre)"
      using mes_prop
      using prod_cases3 by blast 
    then have "assumps ∈ set (map fst (solve_for_lhs_M p a_pre qs subs_pre mat_pre))"
      using reduce_prop(2) by auto
    then have "assumps ∈ set (map fst (construct_rhs_vector_M p a_pre qs subs_pre))"
      unfolding solve_for_lhs_M_def by auto
    then obtain a_rhs_list where "(assumps, a_rhs_list)
    ∈ set (construct_rhs_vector_rec_M p a_pre (pull_out_pairs qs subs_pre))"
      unfolding construct_rhs_vector_M_def by auto
    then have a_pre_subset: "set a_pre ⊆ set assumps"
      using construct_rhs_vector_rec_M_subset_prop[of assumps _ p a_pre "(pull_out_pairs qs subs_pre)"]
      by auto
    have set_a1: "set a1 ⊆ set assumps"
      using a_pre_subset a_pre by auto 
    then have a1_satisfies: "(⋀p n. (p, n) ∈ set a1 ⟹ satisfies_evaluation val p n)"
      using less(3) by blast
    from less.hyps[of ?q1 a1 me1, OF len_q1 mes_prop(1) a1_satisfies]
    have me1_ind: "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q1) = me1"
      using less(4) by blast
    have set_a2: "set a2 ⊆ set assumps"
      using a_pre_subset a_pre by auto 
    then have a2_satisfies: "(⋀p n. (p, n) ∈ set a2 ⟹ satisfies_evaluation val p n)"
      using less(3) by blast
    from less.hyps[of ?q2 a2 me2, OF len_q2 mes_prop(2) a2_satisfies]
    have me2_ind: "calculate_data_R ?eval_p (map (eval_mpoly_poly val) ?q2) = me2"
      using less(4) by blast
    have "a_pre = a1 @ a2 ⟹ me_pre =
      snd (combine_systems_R p (take (length qs div 2) qs, me1)
            (drop (length qs div 2) qs, me2)) ⟹
      snd (combine_systems_R p (take (length qs div 2) qs, me1)
            (drop (length qs div 2) qs, me2)) =
      snd (combine_systems_R (eval_mpoly_poly val p)
            (map (eval_mpoly_poly val) (take (length qs div 2) qs), me1)
            (map (eval_mpoly_poly val) (drop (length qs div 2) qs), me2))"
      using combine_systems_R_snd
      by (metis length_map)
    then have me_pre: "me_pre = snd (combine_systems_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2))"
      using mes_prop(3)
      by (auto)
    obtain mat_pre1 subs_pre1 signs_pre1 where me1_decomp:
      "me1 = (mat_pre1,subs_pre1,signs_pre1)"
      using prod_cases3 by blast
    obtain mat_pre2 subs_pre2 signs_pre2 where me2_decomp:
      "me2 = (mat_pre2,subs_pre2,signs_pre2)"
      using prod_cases3 by blast
    have fst_comb: "fst (combine_systems_R ?eval_p ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2)) = (map (eval_mpoly_poly val) ?q1) @ (map (eval_mpoly_poly val) ?q2)"
    proof -   
      have "fst (combine_systems_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2)) =
        fst (smash_systems_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q1) (map (eval_mpoly_poly val) ?q2) subs_pre1 subs_pre2 signs_pre1 signs_pre2 mat_pre1 mat_pre2)"
        using combining_to_smash_R me1_decomp me2_decomp by force
      then show ?thesis
        unfolding smash_systems_R_def by auto 
    qed
    then have "map (eval_mpoly_poly val) qs = fst (combine_systems_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2))"
      by (metis append_take_drop_id map_append)
    then have me_pre_var:  "(map (eval_mpoly_poly val) qs, me_pre) = (combine_systems_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2))"
      using me_pre by auto 
    have len_hyp: "length (map (eval_mpoly_poly val) qs) > 1"
      using * by auto
    have len_eq: "length (map (eval_mpoly_poly val) qs) = length qs"
      by simp 
    have len_q1_gt0: "length (map (eval_mpoly_poly val) ?q1) > 0"
      using len_hyp len_eq by auto
    have len_q2_gt0: "length (map (eval_mpoly_poly val) ?q2) > 0"
      using len_hyp len_eq by auto
    let ?uni_sys_q1 = "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q1)"
    have sat_props_q1_univ: "satisfies_properties_R ?eval_p (map (eval_mpoly_poly val) ?q1) (get_subsets_R ?uni_sys_q1) (get_signs_R ?uni_sys_q1) (get_matrix_R ?uni_sys_q1)"
      using calculate_data_satisfies_properties_R[of "?eval_p" "(map (eval_mpoly_poly val) (take (length qs div 2) qs))"]
        len_q1_gt0  using less.prems(3) by auto
    let ?uni_sys_q2 = "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q2)"
    have sat_props_q2_univ: "satisfies_properties_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q2) (get_subsets_R ?uni_sys_q2) (get_signs_R ?uni_sys_q2) (get_matrix_R ?uni_sys_q2)"
      using calculate_data_satisfies_properties_R[of "(eval_mpoly_poly val p)" "(map (eval_mpoly_poly val) (drop (length qs div 2) qs))"]
        len_q2_gt0  using less.prems(3)  by auto
    have comb_satisfies: "satisfies_properties_R ?eval_p (?eval_q1@(map (eval_mpoly_poly val) ?q2)) 
  (get_subsets_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2))))) 
  (get_signs_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2))))) 
  (get_matrix_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2)))))"
      using combining_sys_satisfies_properties_R[of ?eval_p ?eval_q1 ?eval_q2] len_q1_gt0 len_q2_gt0 less.prems(3)
        sat_props_q2_univ sat_props_q1_univ
      by auto (* takes a second to load *)
    then have well_def_subs_pre: "all_list_constr_R (get_subsets_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2))))) (length (?eval_q1@?eval_q2))"
      unfolding satisfies_properties_R_def by auto
    have get_subs_pre: "(get_subsets_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2))))) = subs_pre"
      using me_decomp unfolding get_subsets_R_def
      by (metis fst_conv me1_ind me2_ind me_pre_var snd_conv) 
    have well_def: "(⋀Is1 Is2 n. (Is1, Is2) ∈ set (fst (snd me_pre)) ⟹ n ∈ set Is1 ∨ n ∈ set Is2 ⟹ n < length qs)"
      using well_def_subs_pre get_subs_pre 
        all_list_constr_R_matches_well_def[of subs_pre]
      by (smt (verit, ccfv_SIG) fst_comb fst_conv get_subsets_R_def length_map me1_ind me2_ind me_pre_var snd_conv) 
    then have reduce_mat_eq: "mat_eq = reduce_system_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) qs), me_pre)"
      using reduce_system_single_M_univariate[OF reduce_prop(2) less.prems(2)]
      by (metis prod.exhaust_sel) 
    let ?eval_qs = "(map (eval_mpoly_poly val) qs)"
    have "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) = 
     (let q1 = take ((length ?eval_qs) div 2) ?eval_qs; left = calculate_data_R ?eval_p q1;
         q2 = drop ((length ?eval_qs) div 2) ?eval_qs; right = calculate_data_R ?eval_p q2;
         comb = combine_systems_R ?eval_p (q1,left) (q2,right) in
         reduce_system_R ?eval_p comb)"
      using len_hyp
      by (smt (z3) calculate_data_R.simps less_one nat_less_le semiring_norm(136)) 
    moreover have "... = (let q1 =(map (eval_mpoly_poly val) ?q1);
         left = calculate_data_R (eval_mpoly_poly val p) q1;
         q2 = (map (eval_mpoly_poly val) ?q2);
         right = calculate_data_R (eval_mpoly_poly val p) q2
     in Let (combine_systems_R (eval_mpoly_poly val p) (q1, left) (q2, right))
         (reduce_system_R (eval_mpoly_poly val p))) "
      using map_q1 map_q2 by auto 
    moreover have "... = (let q1 =(map (eval_mpoly_poly val) ?q1); left = me1; 
      q2 = (map (eval_mpoly_poly val) ?q2); right = me2 in
      Let (combine_systems_R (eval_mpoly_poly val p) (q1, left) (q2, right))
         (reduce_system_R (eval_mpoly_poly val p)))"
      unfolding Let_def me1_ind me2_ind by auto
    moreover have "... = mat_eq"
      unfolding Let_def reduce_mat_eq me_pre_var by auto  
    ultimately have "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) = mat_eq"
      by auto (* Can take a second to load *)
  }
  ultimately show ?case by blast
qed

lemma calculate_data_M_assumps_univariate:
  assumes mat_eq: "(assumps, mat_eq) ∈ set (calculate_data_assumps_M p qs init_assumps)"
  assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes p_nonzero: "eval_mpoly_poly val p ≠ 0"
  shows "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) = mat_eq"
  using assms
proof (induct "length qs" arbitrary: val p mat_eq assumps qs rule: less_induct)
  case (less qs val p mat_eq assumps) 
  have "length qs = 0 ∨ length qs = 1 ∨ length qs > 1"
    by (meson less_one nat_neq_iff)
  moreover {assume *: "length qs = 0"
    let ?m = "(mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]])"
    let ?subs = "[([], []),([0], []),([], [0])]"
    let ?signs = "[[1],[0],[-1]]"
    let ?eval_p = "eval_mpoly_poly val p"
    have mat_eq_in: "(assumps, mat_eq) ∈ set (calculate_data_assumps_M p [] init_assumps)"
      using * less.prems(1) by auto 
    let ?map_base = "map (λ(assumps,(a,(b,c))). (assumps, (a,b,map (drop 1) c))) (reduce_system_M p [1] (base_case_info_M_assumps init_assumps))"
    have "(assumps, mat_eq) ∈ set ?map_base"
      using mat_eq_in 
      by auto
    then obtain a1 b1 c1 where a1b1c1_prop:
      "(assumps, (a1, (b1, c1))) ∈ set (reduce_system_M p [1] (base_case_info_M_assumps init_assumps))"
      "mat_eq = (a1, (b1, map (drop 1) c1))"
      by auto
    have base_case_well_def: "⋀in_a init_mat_eq Is1 Is2 n subs m signs.
        (in_a, m, subs, signs) ∈ set (base_case_info_M_assumps init_assumps) ⟹
        (Is1, Is2) ∈ set subs ⟹ n ∈ set Is1 ∨ n ∈ set Is2 ⟹ n < length [1]"
      using base_case_with_assumps_info_M_well_def  
      by auto
    have " [1] = map (eval_mpoly_poly val) [1] "
      unfolding eval_mpoly_poly_def eval_mpoly_def 
      by auto
    then have "∃acc mss. (acc,mss) ∈ set ((base_case_info_M_assumps init_assumps)) ∧ (a1, (b1, c1)) = reduce_system_R (eval_mpoly_poly val p) ([1],mss)"
      using reduce_system_M_univariate[of "assumps" "(a1, b1, c1)" p "[1]" "(base_case_info_M_assumps init_assumps)" val "[1]"]
        a1b1c1_prop less(3) base_case_well_def apply (auto)
      by metis
    then obtain acc mss where a1b1c1_connect:
      "(acc,mss) ∈  set ((base_case_info_M_assumps init_assumps))" 
      "(a1, (b1, c1)) = reduce_system_R (eval_mpoly_poly val p) ([1],mss)"
      by auto
    then have mss_is: "mss = base_case_info_R"
      unfolding base_case_info_M_assumps_def 
      using Renegar_Algorithm.base_case_info_R_def Renegar_Algorithm.base_case_info_R_def
      by auto
    obtain a b c where abc_prop: "(a, b, c) = reduction_step_R ?m ?signs ?subs (solve_for_lhs_R ?eval_p [1] ?subs ?m)"
      by (metis reduction_step_R.simps)
    then have "(a, b, c) = (a1, b1, c1)"
      using abc_prop a1b1c1_prop
      by (metis a1b1c1_connect(2) base_case_info_R_def mss_is reduce_system_R.simps) 
    then have mat_eq_is: "(a, b, map (drop (Suc 0)) c) = mat_eq"
      using a1b1c1_prop(2) by (auto) 
    have "(a, b, c) =
  reduction_step_R (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
   [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]
   (solve_for_lhs_R (eval_mpoly_poly val p) [1]
     [([], []), ([0], []), ([], [0])]
     (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]]))"
      using abc_prop
      unfolding base_case_info_R_def
      by (smt (verit) old.prod.case reduce_system_R.simps)
    then have "calculate_data_R ?eval_p (map (eval_mpoly_poly val) qs)= mat_eq"
      using mat_eq_is *
      by (smt (z3) a1b1c1_connect(2) a1b1c1_prop(2) calculate_data_R.simps length_map mss_is split_conv) 
  }
  moreover {assume *: "length qs = 1"
    have meq: "(assumps, mat_eq) ∈ set (reduce_system_M p qs (base_case_info_M_assumps init_assumps))"
      using "*" le_eq_less_or_eq less(2) one_neq_zero by auto
    have **: "⋀init_assumps init_mat_eq Is1 Is2 n subs m signs.
      (init_assumps, m, subs, signs) ∈ set (base_case_info_M_assumps init_assumps) ⟹
      (Is1, Is2) ∈ set subs ⟹
      n ∈ set Is1 ∨ n ∈ set Is2 ⟹
      n < length qs" unfolding *
      using base_case_with_assumps_info_M_well_def
      by meson
    from reduce_system_M_univariate[OF meq less(3), of " map (eval_mpoly_poly val)
   qs"]
    obtain acc mss where ams: "(acc,mss) ∈ set (base_case_info_M_assumps init_assumps)" 
      "mat_eq = reduce_system_R (eval_mpoly_poly val p)
      (map (eval_mpoly_poly val) qs, mss)"
      using "**"
      apply (auto) 
      by (smt (z3) "*" base_case_with_assumps_info_M_well_def) 
    then have "mss = base_case_info_R" unfolding base_case_info_M_assumps_def 
      using Renegar_Algorithm.base_case_info_R_def Renegar_Algorithm.base_case_info_R_def
      by auto
    then have "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) = mat_eq"
      using ams * by simp
  }
    (* Inductive case: progress by breaking down, using IH, then piecing back together.
      It's the reduction of a combination of two smaller matrix equation pieces. *)
  moreover {assume *: "length qs  > 1"
    have inset: "(assumps, mat_eq) ∈ set (calculate_data_assumps_M p qs init_assumps)"
      using less.prems(1) 
      by auto 
    let ?len = "length qs"
    let ?q1 = "take (?len div 2) qs"
    let ?q2 = "drop (?len div 2) qs"
    let ?left = "calculate_data_assumps_M p ?q1 init_assumps"
    let ?right = "calculate_data_assumps_M p ?q2 init_assumps"
    let ?comb = "combine_systems_M p ?q1 ?left ?q2 ?right"
    let ?eval_p = "(eval_mpoly_poly val p)"
    let ?eval_q1 = "(map (eval_mpoly_poly val) ?q1)"
    let ?eval_q2 = "(map (eval_mpoly_poly val) ?q2)"
    have map_q1: "map (eval_mpoly_poly val) ?q1 = 
      (take (length (map (eval_mpoly_poly val) qs) div 2) (map (eval_mpoly_poly val) qs))"
      by (auto simp add: take_map) 
    have map_q2: "map (eval_mpoly_poly val) ?q2 = 
      (drop (length (map (eval_mpoly_poly val) qs) div 2) (map (eval_mpoly_poly val) qs))"
      by (auto simp add: drop_map) 
    have "fst ?comb = qs" 
      by auto
    then have "(assumps, mat_eq) ∈ set (reduce_system_M p qs (snd ?comb))"
      using inset *
      by (smt (z3) calculate_data_assumps_M.simps gr_implies_not0 less_one nat_less_le) 
    then have "(assumps, mat_eq) ∈ set (concat (map (reduce_system_single_M p qs) (snd ?comb)))"
      by (metis reduce_system_M.simps)
    then have "∃sys. sys ∈ set (snd ?comb) ∧ (assumps, mat_eq) ∈ set(reduce_system_single_M p qs sys)"
      using concat_map_in_set in_set_member
      by (metis nth_mem) 
    then obtain a_pre me_pre  where reduce_prop: "(a_pre, me_pre) ∈ set (snd ?comb)"
      "(assumps, mat_eq) ∈ set(reduce_system_single_M p qs (a_pre, me_pre))"
      by fastforce 
    then obtain a1 me1 a2 me2 where mes_prop: "(a1, me1) ∈ set ?left"
      "(a2, me2) ∈ set ?right"
      "(a_pre, me_pre) = combine_systems_single_M p ?q1 (a1, me1) ?q2 (a2, me2)"
      by auto
    then have a_pre: "a_pre = a1@a2" 
      by auto 
    have lengt: "length qs div 2 ≥ 1"
      using * by auto
    then have len_q1: "length ?q1 < length qs"
      by auto
    have len_q2: "length ?q2 < length qs"
      using lengt by auto
    obtain mat_pre subs_pre signs_pre where me_decomp:
      "me_pre = (mat_pre,subs_pre,signs_pre)"
      using mes_prop
      using prod_cases3 by blast 
    then have "assumps ∈ set (map fst (solve_for_lhs_M p a_pre qs subs_pre mat_pre))"
      using reduce_prop(2) by auto
    then have "assumps ∈ set (map fst (construct_rhs_vector_M p a_pre qs subs_pre))"
      unfolding solve_for_lhs_M_def by auto
    then obtain a_rhs_list where "(assumps, a_rhs_list)
    ∈ set (construct_rhs_vector_rec_M p a_pre (pull_out_pairs qs subs_pre))"
      unfolding construct_rhs_vector_M_def by auto
    then have a_pre_subset: "set a_pre ⊆ set assumps"
      using construct_rhs_vector_rec_M_subset_prop[of assumps _ p a_pre "(pull_out_pairs qs subs_pre)"]
      by auto
    have set_a1: "set a1 ⊆ set assumps"
      using a_pre_subset a_pre by auto 
    then have a1_satisfies: "(⋀p n. (p, n) ∈ set a1 ⟹ satisfies_evaluation val p n)"
      using less(3) by blast
    from less.hyps[of ?q1 a1 me1, OF len_q1 mes_prop(1) a1_satisfies]
    have me1_ind: "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q1) = me1"
      using less(4) by blast
    have set_a2: "set a2 ⊆ set assumps"
      using a_pre_subset a_pre by auto 
    then have a2_satisfies: "(⋀p n. (p, n) ∈ set a2 ⟹ satisfies_evaluation val p n)"
      using less(3) by blast
    from less.hyps[of ?q2 a2 me2, OF len_q2 mes_prop(2) a2_satisfies]
    have me2_ind: "calculate_data_R ?eval_p (map (eval_mpoly_poly val) ?q2) = me2"
      using less(4) by blast
    have me_pre: "me_pre = snd (combine_systems_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2))"
      using mes_prop(3) combine_systems_R_snd length_map
      by (metis combine_systems_single_M.simps snd_conv) 
    obtain mat_pre1 subs_pre1 signs_pre1 where me1_decomp:
      "me1 = (mat_pre1,subs_pre1,signs_pre1)"
      using prod_cases3 by blast
    obtain mat_pre2 subs_pre2 signs_pre2 where me2_decomp:
      "me2 = (mat_pre2,subs_pre2,signs_pre2)"
      using prod_cases3 by blast
    have fst_comb: "fst (combine_systems_R ?eval_p ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2)) = (map (eval_mpoly_poly val) ?q1) @ (map (eval_mpoly_poly val) ?q2)"
    proof -   
      have "fst (combine_systems_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2)) =
        fst (smash_systems_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q1) (map (eval_mpoly_poly val) ?q2) subs_pre1 subs_pre2 signs_pre1 signs_pre2 mat_pre1 mat_pre2)"
        using combining_to_smash_R me1_decomp me2_decomp by force
      then show ?thesis
        unfolding smash_systems_R_def by auto 
    qed
    then have "map (eval_mpoly_poly val) qs = fst (combine_systems_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2))"
      by (metis append_take_drop_id map_append)
    then have me_pre_var:  "(map (eval_mpoly_poly val) qs, me_pre) = (combine_systems_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) ?q1), me1) ((map (eval_mpoly_poly val) ?q2), me2))"
      using me_pre by auto 
    have len_hyp: "length (map (eval_mpoly_poly val) qs) > 1"
      using * by auto
    have len_eq: "length (map (eval_mpoly_poly val) qs) = length qs"
      by simp 
    have len_q1_gt0: "length (map (eval_mpoly_poly val) ?q1) > 0"
      using len_hyp len_eq by auto
    have len_q2_gt0: "length (map (eval_mpoly_poly val) ?q2) > 0"
      using len_hyp len_eq by auto
    let ?uni_sys_q1 = "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q1)"
    have sat_props_q1_univ: "satisfies_properties_R ?eval_p (map (eval_mpoly_poly val) ?q1) (get_subsets_R ?uni_sys_q1) (get_signs_R ?uni_sys_q1) (get_matrix_R ?uni_sys_q1)"
      using calculate_data_satisfies_properties_R[of "?eval_p" "(map (eval_mpoly_poly val) (take (length qs div 2) qs))"]
        len_q1_gt0  using less.prems(3) by auto
    let ?uni_sys_q2 = "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q2)"
    have sat_props_q2_univ: "satisfies_properties_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) ?q2) (get_subsets_R ?uni_sys_q2) (get_signs_R ?uni_sys_q2) (get_matrix_R ?uni_sys_q2)"
      using calculate_data_satisfies_properties_R[of "(eval_mpoly_poly val p)" "(map (eval_mpoly_poly val) (drop (length qs div 2) qs))"]
        len_q2_gt0  using less.prems(3)  by auto
    have comb_satisfies: "satisfies_properties_R ?eval_p (?eval_q1@(map (eval_mpoly_poly val) ?q2)) 
  (get_subsets_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2))))) 
  (get_signs_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2))))) 
  (get_matrix_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2)))))"
      using combining_sys_satisfies_properties_R[of ?eval_p ?eval_q1 ?eval_q2] len_q1_gt0 len_q2_gt0 less.prems(3)
        sat_props_q2_univ sat_props_q1_univ 
      by auto  (* takes a second to load *)
    then have well_def_subs_pre: "all_list_constr_R (get_subsets_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2))))) (length (?eval_q1@?eval_q2))"
      unfolding satisfies_properties_R_def by auto
    have get_subs_pre: "(get_subsets_R (snd ((combine_systems_R ?eval_p (?eval_q1,?uni_sys_q1) (?eval_q2,?uni_sys_q2))))) = subs_pre"
      using me_decomp unfolding get_subsets_R_def
      by (metis fst_conv me1_ind me2_ind me_pre_var snd_conv) 
    have well_def: "(⋀Is1 Is2 n. (Is1, Is2) ∈ set (fst (snd me_pre)) ⟹ n ∈ set Is1 ∨ n ∈ set Is2 ⟹ n < length qs)"
      using well_def_subs_pre get_subs_pre 
        all_list_constr_R_matches_well_def[of subs_pre]
      by (smt (verit, ccfv_SIG) fst_comb fst_conv get_subsets_R_def length_map me1_ind me2_ind me_pre_var snd_conv) 
    then have reduce_mat_eq: "mat_eq =  reduce_system_R (eval_mpoly_poly val p) ((map (eval_mpoly_poly val) qs), me_pre)"
      using reduce_system_single_M_univariate[OF reduce_prop(2) less.prems(2)]
      by (metis prod.exhaust_sel) 
    let ?eval_qs = "(map (eval_mpoly_poly val) qs)"
    have "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) = 
     (let q1 = take ((length ?eval_qs) div 2) ?eval_qs; left = calculate_data_R ?eval_p q1;
         q2 = drop ((length ?eval_qs) div 2) ?eval_qs; right = calculate_data_R ?eval_p q2;
         comb = combine_systems_R ?eval_p (q1,left) (q2,right) in
         reduce_system_R ?eval_p comb)"
      using len_hyp
      by (smt (z3) calculate_data_R.simps less_one nat_less_le semiring_norm(136)) 
    moreover have "... = (let q1 =(map (eval_mpoly_poly val) ?q1);
         left = calculate_data_R (eval_mpoly_poly val p) q1;
         q2 = (map (eval_mpoly_poly val) ?q2);
         right = calculate_data_R (eval_mpoly_poly val p) q2
     in Let (combine_systems_R (eval_mpoly_poly val p) (q1, left) (q2, right))
         (reduce_system_R (eval_mpoly_poly val p))) "
      using map_q1 map_q2 by auto 
    moreover have "... = (let q1 =(map (eval_mpoly_poly val) ?q1); left = me1; 
      q2 = (map (eval_mpoly_poly val) ?q2); right = me2 in
      Let (combine_systems_R (eval_mpoly_poly val p) (q1, left) (q2, right))
         (reduce_system_R (eval_mpoly_poly val p)))"
      unfolding Let_def me1_ind me2_ind by auto
    moreover have "... = mat_eq"
      unfolding Let_def reduce_mat_eq me_pre_var by auto  
    ultimately have "calculate_data_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs) = mat_eq"
      by auto
  }
  ultimately show ?case by blast
qed

lemma calculate_data_gives_signs_at_roots:
  assumes "(assumps, signs) ∈ set (calculate_data_to_signs (calculate_data_M p qs))"
  assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes "eval_mpoly_poly val p ≠ 0"
  shows "signs = find_consistent_signs_at_roots_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs)"
  using assms calculate_data_M_univariate 
  unfolding find_consistent_signs_at_roots_R_def by auto

lemma calculate_data_gives_noncomp_signs_at_roots:
  assumes "(assumps, signs) ∈ set (calculate_data_to_signs (calculate_data_M p qs))"
  assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes "eval_mpoly_poly val p ≠ 0"
  shows "set signs = set (characterize_consistent_signs_at_roots (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs))"
  using assms find_consistent_signs_at_roots_R calculate_data_gives_signs_at_roots
  by metis

lemma calculate_data_assumps_gives_signs_at_roots:
  assumes "(assumps, signs) ∈ set (calculate_data_to_signs (calculate_data_assumps_M p qs init_assumps))"
  assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes "eval_mpoly_poly val p ≠ 0"
  shows "signs = find_consistent_signs_at_roots_R (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs)"
  using assms calculate_data_M_assumps_univariate 
  unfolding find_consistent_signs_at_roots_R_def 
  by auto

lemma calculate_data_assumps_gives_noncomp_signs_at_roots:
  assumes "(assumps, signs) ∈ set (calculate_data_to_signs (calculate_data_assumps_M p qs init_assumps))"
  assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
  assumes "eval_mpoly_poly val p ≠ 0"
  shows "set signs = set (characterize_consistent_signs_at_roots (eval_mpoly_poly val p) (map (eval_mpoly_poly val) qs))"
  using assms find_consistent_signs_at_roots_R calculate_data_assumps_gives_signs_at_roots
  by metis 

end