[STATEMENT]
lemma fs_int_mu_d_Z:
  assumes j: "j \<le> ii" and ii: "ii < m"
  shows "of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
have id: "of_int (d fs (Suc j)) = gs.Gramian_determinant (RAT fs) (Suc j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) = gs.d (Suc j)
[PROOF STEP]
unfolding d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (gs.Gramian_determinant fs (Suc j)) = gs.d (Suc j)
[PROOF STEP]
by (rule of_int_Gramian_determinant[symmetric], insert j ii , auto)
[PROOF STATE]
proof (state)
this:
rat_of_int (d fs (Suc j)) = gs.d (Suc j)

goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
have "of_int_hom.vec_hom (fs ! j) $ i \<in> \<int>" if "i < n" "j < length fs" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom (fs ! j) $ i \<in> \<int>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < n
j < length fs

goal (1 subgoal):
 1. of_int_hom.vec_hom (fs ! j) $ i \<in> \<int>
[PROOF STEP]
by (intro vec_hom_Ints) auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < n; ?j2 < length fs\<rbrakk> \<Longrightarrow> of_int_hom.vec_hom (fs ! ?j2) $ ?i2 \<in> \<int>

goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i2 < n; ?j2 < length fs\<rbrakk> \<Longrightarrow> of_int_hom.vec_hom (fs ! ?j2) $ ?i2 \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i2 < n; ?j2 < length fs\<rbrakk> \<Longrightarrow> of_int_hom.vec_hom (fs ! ?j2) $ ?i2 \<in> \<int>

goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i2 < n; ?j2 < length fs\<rbrakk> \<Longrightarrow> of_int_hom.vec_hom (fs ! ?j2) $ ?i2 \<in> \<int>

goal (1 subgoal):
 1. gs.d (Suc j) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
using j ii
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i2 < n; ?j2 < length fs\<rbrakk> \<Longrightarrow> of_int_hom.vec_hom (fs ! ?j2) $ ?i2 \<in> \<int>
j \<le> ii
ii < length fs

goal (1 subgoal):
 1. gs.d (Suc j) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
unfolding gs.lin_indpt_list_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i2 < n; ?j2 < length fs\<rbrakk> \<Longrightarrow> of_int_hom.vec_hom (fs ! ?j2) $ ?i2 \<in> \<int>
j \<le> ii
ii < length fs

goal (1 subgoal):
 1. gs.d (Suc j) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
by (intro gs.d_mu_Ints) (auto)
[PROOF STATE]
proof (state)
this:
rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fs_int_mu_d_Z_m_m:
  assumes j: "j < m" and ii: "ii < m"
  shows "of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
proof (cases "j \<le> ii")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j \<le> ii \<Longrightarrow> rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
 2. \<not> j \<le> ii \<Longrightarrow> rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j \<le> ii

goal (2 subgoals):
 1. j \<le> ii \<Longrightarrow> rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
 2. \<not> j \<le> ii \<Longrightarrow> rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<le> ii

goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
using fs_int_mu_d_Z[OF True ii]
[PROOF STATE]
proof (prove)
using this:
j \<le> ii
rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>

goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>

goal (1 subgoal):
 1. \<not> j \<le> ii \<Longrightarrow> rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j \<le> ii \<Longrightarrow> rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> j \<le> ii

goal (1 subgoal):
 1. \<not> j \<le> ii \<Longrightarrow> rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> j \<le> ii

goal (1 subgoal):
 1. rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>
[PROOF STEP]
by (simp add: gs.\<mu>.simps)
[PROOF STATE]
proof (state)
this:
rat_of_int (d fs (Suc j)) * gs.\<mu> ii j \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sq_norm_fs_via_sum_mu_gso: assumes i: "i < m"
  shows "of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
let ?G = "map (gs.gso) [0 ..< m]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
let ?gso = "\<lambda> fs j. ?G ! j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
have "of_int \<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>RAT fs ! i\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>map of_int_hom.vec_hom fs ! i\<parallel>\<^sup>2
[PROOF STEP]
unfolding sq_norm_of_int[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>of_int_hom.vec_hom (fs ! i)\<parallel>\<^sup>2 = \<parallel>map of_int_hom.vec_hom fs ! i\<parallel>\<^sup>2
[PROOF STEP]
using insert i
[PROOF STATE]
proof (prove)
using this:
ListMem ?x ?xs \<Longrightarrow> ListMem ?x (?y # ?xs)
i < length fs

goal (1 subgoal):
 1. \<parallel>of_int_hom.vec_hom (fs ! i)\<parallel>\<^sup>2 = \<parallel>map of_int_hom.vec_hom fs ! i\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>map of_int_hom.vec_hom fs ! i\<parallel>\<^sup>2

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>map of_int_hom.vec_hom fs ! i\<parallel>\<^sup>2

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
have "RAT fs ! i = gs.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map of_int_hom.vec_hom fs ! i = gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i])
[PROOF STEP]
using gs.fi_is_sum_of_mu_gso i
[PROOF STATE]
proof (prove)
using this:
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> map of_int_hom.vec_hom fs ! ?i = gs.M.sumlist (map (\<lambda>j. gs.\<mu> ?i j \<cdot>\<^sub>v gs.gso j) [0..<Suc ?i])
i < length fs

goal (1 subgoal):
 1. map of_int_hom.vec_hom fs ! i = gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map of_int_hom.vec_hom fs ! i = gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i])

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map of_int_hom.vec_hom fs ! i = gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i])

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
have id: "map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i] = map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v ?gso fs j) [0..<Suc i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i] = map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i]
[PROOF STEP]
by (rule nth_equalityI, insert i, auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i] = map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i]

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i] = map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i]

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
have "sq_norm (gs.sumlist \<dots>) = sum_list (map sq_norm (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i])\<parallel>\<^sup>2 = sum_list (map sq_norm (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i]))
[PROOF STEP]
unfolding map_map o_def sq_norm_smult_vec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i])\<parallel>\<^sup>2 = (\<Sum>x\<leftarrow>[0..<Suc i]. sq_norm_conjugate (gs.\<mu> i x) * \<parallel>gs.gso x\<parallel>\<^sup>2)
[PROOF STEP]
unfolding sq_norm_vec_as_cscalar_prod cscalar_prod_is_scalar_prod conjugate_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i]) \<bullet> gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i]) = (\<Sum>x\<leftarrow>[0..<Suc i]. gs.\<mu> i x * gs.\<mu> i x * (gs.gso x \<bullet> gs.gso x))
[PROOF STEP]
proof (subst gs.scalar_prod_lincomb_orthogonal)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. orthogonal (map gs.gso [0..<length fs])
 2. set (map gs.gso [0..<length fs]) \<subseteq> carrier_vec n
 3. Suc i \<le> length (map gs.gso [0..<length fs])
 4. (\<Sum>ia\<leftarrow>[0..<Suc i]. gs.\<mu> i ia * gs.\<mu> i ia * (map gs.gso [0..<length fs] ! ia \<bullet> map gs.gso [0..<length fs] ! ia)) = (\<Sum>x\<leftarrow>[0..<Suc i]. gs.\<mu> i x * gs.\<mu> i x * (gs.gso x \<bullet> gs.gso x))
[PROOF STEP]
show "Suc i \<le> length ?G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc i \<le> length (map gs.gso [0..<length fs])
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. Suc i \<le> length (map gs.gso [0..<length fs])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i \<le> length (map gs.gso [0..<length fs])

goal (3 subgoals):
 1. orthogonal (map gs.gso [0..<length fs])
 2. set (map gs.gso [0..<length fs]) \<subseteq> carrier_vec n
 3. (\<Sum>ia\<leftarrow>[0..<Suc i]. gs.\<mu> i ia * gs.\<mu> i ia * (map gs.gso [0..<length fs] ! ia \<bullet> map gs.gso [0..<length fs] ! ia)) = (\<Sum>x\<leftarrow>[0..<Suc i]. gs.\<mu> i x * gs.\<mu> i x * (gs.gso x \<bullet> gs.gso x))
[PROOF STEP]
show "set ?G \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map gs.gso [0..<length fs]) \<subseteq> carrier_vec n
[PROOF STEP]
using gs.gso_carrier
[PROOF STATE]
proof (prove)
using this:
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> gs.gso ?i \<in> carrier_vec n

goal (1 subgoal):
 1. set (map gs.gso [0..<length fs]) \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (map gs.gso [0..<length fs]) \<subseteq> carrier_vec n

goal (2 subgoals):
 1. orthogonal (map gs.gso [0..<length fs])
 2. (\<Sum>ia\<leftarrow>[0..<Suc i]. gs.\<mu> i ia * gs.\<mu> i ia * (map gs.gso [0..<length fs] ! ia \<bullet> map gs.gso [0..<length fs] ! ia)) = (\<Sum>x\<leftarrow>[0..<Suc i]. gs.\<mu> i x * gs.\<mu> i x * (gs.gso x \<bullet> gs.gso x))
[PROOF STEP]
show "orthogonal ?G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal (map gs.gso [0..<length fs])
[PROOF STEP]
using gs.orthogonal_gso
[PROOF STATE]
proof (prove)
using this:
orthogonal (map gs.gso [0..<length (map of_int_hom.vec_hom fs)])

goal (1 subgoal):
 1. orthogonal (map gs.gso [0..<length fs])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orthogonal (map gs.gso [0..<length fs])

goal (1 subgoal):
 1. (\<Sum>ia\<leftarrow>[0..<Suc i]. gs.\<mu> i ia * gs.\<mu> i ia * (map gs.gso [0..<length fs] ! ia \<bullet> map gs.gso [0..<length fs] ! ia)) = (\<Sum>x\<leftarrow>[0..<Suc i]. gs.\<mu> i x * gs.\<mu> i x * (gs.gso x \<bullet> gs.gso x))
[PROOF STEP]
qed (rule arg_cong[of _ _ sum_list], intro nth_equalityI, insert i, auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
\<parallel>gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i])\<parallel>\<^sup>2 = sum_list (map sq_norm (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i]))

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>gs.M.sumlist (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v map gs.gso [0..<length fs] ! j) [0..<Suc i])\<parallel>\<^sup>2 = sum_list (map sq_norm (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i]))

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
have "map sq_norm (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i]) = map (\<lambda>j. (gs.\<mu> i j)^2 * sq_norm (gs.gso j)) [0..<Suc i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map sq_norm (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i]) = map (\<lambda>j. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2) [0..<Suc i]
[PROOF STEP]
unfolding map_map o_def sq_norm_smult_vec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>x. sq_norm_conjugate (gs.\<mu> i x) * \<parallel>gs.gso x\<parallel>\<^sup>2) [0..<Suc i] = map (\<lambda>j. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2) [0..<Suc i]
[PROOF STEP]
by (rule map_cong, auto simp: power2_eq_square)
[PROOF STATE]
proof (state)
this:
map sq_norm (map (\<lambda>j. gs.\<mu> i j \<cdot>\<^sub>v gs.gso j) [0..<Suc i]) = map (\<lambda>j. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2) [0..<Suc i]

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)

goal (1 subgoal):
 1. rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rat_of_int \<parallel>fs ! i\<parallel>\<^sup>2 = (\<Sum>j\<leftarrow>[0..<Suc i]. (gs.\<mu> i j)\<^sup>2 * \<parallel>gs.gso j\<parallel>\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma d\<mu>: assumes "j < m" "ii < m"
  shows "of_int (d\<mu> ii j) = of_int (d fs (Suc j)) * gs.\<mu> ii j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (d\<mu> ii j) = rat_of_int (d fs (Suc j)) * gs.\<mu> ii j
[PROOF STEP]
unfolding d\<mu>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (int_of_rat (rat_of_int (d fs (Suc j)) * gs.\<mu> ii j)) = rat_of_int (d fs (Suc j)) * gs.\<mu> ii j
[PROOF STEP]
using fs_int_mu_d_Z_m_m assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?j < length fs; ?ii < length fs\<rbrakk> \<Longrightarrow> rat_of_int (d fs (Suc ?j)) * gs.\<mu> ?ii ?j \<in> \<int>
j < length fs
ii < length fs

goal (1 subgoal):
 1. rat_of_int (int_of_rat (rat_of_int (d fs (Suc j)) * gs.\<mu> ii j)) = rat_of_int (d fs (Suc j)) * gs.\<mu> ii j
[PROOF STEP]
by auto


[STATEMENT]
lemma add_shift:"x+y = z \<longleftrightarrow> Some x +\<^sub>o Some y = Some z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + y = z) = (Some x +\<^sub>o Some y = Some z)
[PROOF STEP]
by (simp add: add_def)


[STATEMENT]
lemma mul_shift:"x*y = z \<longleftrightarrow> Some x *\<^sub>o Some y = Some z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y = z) = (Some x *\<^sub>o Some y = Some z)
[PROOF STEP]
by (simp add: mul_def)


[STATEMENT]
lemma power_shift:"x^y = z \<longleftrightarrow> Some x ^\<^sub>o Some y = Some z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ^ y = z) = (Some x ^\<^sub>o Some y = Some z)
[PROOF STEP]
by (simp add: power_def)


[STATEMENT]
lemma less_shift: "x < y \<longleftrightarrow> Some x <\<^sub>o Some y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < y) = Some x <\<^sub>o Some y
[PROOF STEP]
by simp


[STATEMENT]
lemma lesseq_shift: "x \<le> y \<longleftrightarrow> Some x \<le>\<^sub>o Some y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> y) = Some x \<le>\<^sub>o Some y
[PROOF STEP]
by simp


[STATEMENT]
lemma greater_shift: "x > y \<longleftrightarrow> Some x >\<^sub>o Some y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y < x) = Some x >\<^sub>o Some y
[PROOF STEP]
by simp


[STATEMENT]
lemma maxt_member: "invar_vebt t n \<Longrightarrow> vebt_maxt t = Some maxi \<Longrightarrow> vebt_member t maxi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; vebt_maxt t = Some maxi\<rbrakk> \<Longrightarrow> vebt_member t maxi
[PROOF STEP]
proof(induction t n  arbitrary: maxi rule: invar_vebt.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b maxi. vebt_maxt (Leaf a b) = Some maxi \<Longrightarrow> vebt_member (Leaf a b) maxi
 2. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 3. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 4. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 5. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
case (1 a b)
[PROOF STATE]
proof (state)
this:
vebt_maxt (Leaf a b) = Some maxi

goal (5 subgoals):
 1. \<And>a b maxi. vebt_maxt (Leaf a b) = Some maxi \<Longrightarrow> vebt_member (Leaf a b) maxi
 2. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 3. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 4. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 5. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vebt_maxt (Leaf a b) = Some maxi
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vebt_maxt (Leaf a b) = Some maxi

goal (1 subgoal):
 1. vebt_member (Leaf a b) maxi
[PROOF STEP]
by (metis VEBT_Member.vebt_member.simps(1) vebt_maxt.simps(1) option.distinct(1) option.inject zero_neq_one)
[PROOF STATE]
proof (state)
this:
vebt_member (Leaf a b) maxi

goal (4 subgoals):
 1. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 2. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 3. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 4. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 2. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 3. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 4. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
case (2 treeList n summary m deg)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = n
deg = n + m
\<nexists>i. both_member_options summary i
\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x
vebt_maxt (Node None deg treeList summary) = Some maxi

goal (4 subgoals):
 1. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 2. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 3. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 4. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = n
deg = n + m
\<nexists>i. both_member_options summary i
\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x
vebt_maxt (Node None deg treeList summary) = Some maxi
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = n
deg = n + m
\<nexists>i. both_member_options summary i
\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x
vebt_maxt (Node None deg treeList summary) = Some maxi

goal (1 subgoal):
 1. vebt_member (Node None deg treeList summary) maxi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vebt_member (Node None deg treeList summary) maxi

goal (3 subgoals):
 1. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 2. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 3. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 2. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 3. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
case (3 treeList n summary m deg)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = Suc n
deg = n + m
\<nexists>i. both_member_options summary i
\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x
vebt_maxt (Node None deg treeList summary) = Some maxi

goal (3 subgoals):
 1. \<And>treeList n summary m deg maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<nexists>i. both_member_options summary i; \<forall>t\<in>set treeList. \<nexists>x. both_member_options t x; vebt_maxt (Node None deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node None deg treeList summary) maxi
 2. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 3. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = Suc n
deg = n + m
\<nexists>i. both_member_options summary i
\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x
vebt_maxt (Node None deg treeList summary) = Some maxi
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = Suc n
deg = n + m
\<nexists>i. both_member_options summary i
\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x
vebt_maxt (Node None deg treeList summary) = Some maxi

goal (1 subgoal):
 1. vebt_member (Node None deg treeList summary) maxi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vebt_member (Node None deg treeList summary) maxi

goal (2 subgoals):
 1. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 2. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 2. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
case (4 treeList n summary m deg mi ma)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = n
deg = n + m
\<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i
mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x)
mi \<le> ma
ma < 2 ^ deg
mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma))
vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi

goal (2 subgoals):
 1. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 2. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
hence "deg \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = n
deg = n + m
\<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i
mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x)
mi \<le> ma
ma < 2 ^ deg
mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma))
vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi

goal (1 subgoal):
 1. 2 \<le> deg
[PROOF STEP]
by (metis One_nat_def Suc_le_eq add_mono deg_not_0 numeral_2_eq_2 plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
2 \<le> deg

goal (2 subgoals):
 1. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
 2. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> deg
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
2 \<le> deg

goal (1 subgoal):
 1. vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
by (metis "4.prems" VEBT_Member.vebt_member.simps(5) Suc_diff_Suc Suc_pred lessI less_le_trans vebt_maxt.simps(3) numeral_2_eq_2 option.inject zero_less_Suc)
[PROOF STATE]
proof (state)
this:
vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi

goal (1 subgoal):
 1. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
case (5 treeList n summary m deg mi ma)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = Suc n
deg = n + m
\<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i
mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x)
mi \<le> ma
ma < 2 ^ deg
mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma))
vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi

goal (1 subgoal):
 1. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
hence "deg \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x)
vebt_maxt summary = Some ?maxi \<Longrightarrow> vebt_member summary ?maxi
invar_vebt summary m
length treeList = 2 ^ m
m = Suc n
deg = n + m
\<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i
mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x)
mi \<le> ma
ma < 2 ^ deg
mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma))
vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi

goal (1 subgoal):
 1. 2 \<le> deg
[PROOF STEP]
by (metis Suc_leI le_add2 less_add_same_cancel2 less_le_trans not_less_iff_gr_or_eq not_one_le_zero numeral_2_eq_2 plus_1_eq_Suc set_n_deg_not_0)
[PROOF STATE]
proof (state)
this:
2 \<le> deg

goal (1 subgoal):
 1. \<And>treeList n summary m deg mi ma maxi. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n \<and> (\<forall>x. vebt_maxt t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_maxt summary = Some maxi \<Longrightarrow> vebt_member summary maxi; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. (\<exists>x. both_member_options (treeList ! i) x) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<nexists>x. both_member_options t x); mi \<le> ma; ma < 2 ^ deg; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma n = i \<longrightarrow> both_member_options (treeList ! i) (low ma n)) \<and> (\<forall>x. high x n = i \<and> both_member_options (treeList ! i) (low x n) \<longrightarrow> mi < x \<and> x \<le> ma)); vebt_maxt (Node (Some (mi, ma)) deg treeList summary) = Some maxi\<rbrakk> \<Longrightarrow> vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> deg
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
2 \<le> deg

goal (1 subgoal):
 1. vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
by (metis "5.prems" VEBT_Member.vebt_member.simps(5) add_2_eq_Suc le_add_diff_inverse vebt_maxt.simps(3) option.inject)
[PROOF STATE]
proof (state)
this:
vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maxt_corr_help: "invar_vebt t n \<Longrightarrow> vebt_maxt t = Some maxi \<Longrightarrow> vebt_member t x \<Longrightarrow> maxi \<ge> x "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; vebt_maxt t = Some maxi; vebt_member t x\<rbrakk> \<Longrightarrow> x \<le> maxi
[PROOF STEP]
by (smt VEBT_Member.vebt_member.simps(1) le_less vebt_maxt.elims member_inv mi_ma_2_deg option.simps(1) option.simps(3) zero_le_one)


[STATEMENT]
lemma maxt_corr_help_empty: "invar_vebt t n \<Longrightarrow> vebt_maxt t = None \<Longrightarrow> set_vebt' t = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; vebt_maxt t = None\<rbrakk> \<Longrightarrow> set_vebt' t = {}
[PROOF STEP]
by (metis (full_types) VEBT_Member.vebt_member.simps(1) empty_Collect_eq vebt_maxt.elims minNull.simps(4) min_Null_member option.distinct(1) set_vebt'_def)


[STATEMENT]
theorem maxt_corr:assumes "invar_vebt t n" and "vebt_maxt t = Some x" shows "max_in_set (set_vebt' t) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_in_set (set_vebt' t) x
[PROOF STEP]
unfolding set_vebt'_def Max_def max_in_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Collect (vebt_member t) \<and> (\<forall>y\<in>Collect (vebt_member t). y \<le> x)
[PROOF STEP]
using assms(1) assms(2) maxt_corr_help maxt_member
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n
vebt_maxt t = Some x
\<lbrakk>invar_vebt ?t ?n; vebt_maxt ?t = Some ?maxi; vebt_member ?t ?x\<rbrakk> \<Longrightarrow> ?x \<le> ?maxi
\<lbrakk>invar_vebt ?t ?n; vebt_maxt ?t = Some ?maxi\<rbrakk> \<Longrightarrow> vebt_member ?t ?maxi

goal (1 subgoal):
 1. x \<in> Collect (vebt_member t) \<and> (\<forall>y\<in>Collect (vebt_member t). y \<le> x)
[PROOF STEP]
by blast


[STATEMENT]
theorem maxt_sound:assumes "invar_vebt t n" and  "max_in_set (set_vebt' t) x" shows "vebt_maxt t = Some x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_maxt t = Some x
[PROOF STEP]
by (metis (no_types, opaque_lifting) assms(1) assms(2) empty_Collect_eq le_less max_in_set_def
 maxt_corr_help maxt_corr_help_empty maxt_member mem_Collect_eq not_le option.exhaust set_vebt'_def)