[STATEMENT]
lemma mint_member: "invar_vebt t n \<Longrightarrow> vebt_mint t = Some maxi \<Longrightarrow> vebt_member t maxi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint (Leaf a b) = Some maxi

goal (5 subgoals):
 1. \<And>a b maxi. vebt_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint (Leaf a b) = Some maxi
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vebt_mint (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_mint.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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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) One_nat_def Suc_diff_Suc Suc_pred dual_order.strict_trans1 le_imp_less_Suc le_numeral_extra(4) vebt_mint.simps(3) numeral_2_eq_2 option.inject zero_le_one)
[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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x)
vebt_mint 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_mint (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_mint t = Some x \<longrightarrow> vebt_member t x); invar_vebt summary m; \<And>maxi. vebt_mint 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_mint (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]
using  "5.prems" VEBT_Member.vebt_member.simps(5) add_2_eq_Suc  le_add_diff_inverse vebt_mint.simps(3)
[PROOF STATE]
proof (prove)
using this:
2 \<le> deg
vebt_mint (Node (Some (mi, ma)) deg treeList summary) = Some maxi
vebt_member (Node (Some (?mi, ?ma)) (Suc (Suc ?va)) ?treeList ?summary) ?x = (if ?x = ?mi then True else if ?x = ?ma then True else if ?x < ?mi then False else if ?ma < ?x then False else let h = high ?x (Suc (Suc ?va) div 2); l = low ?x (Suc (Suc ?va) div 2) in if h < length ?treeList then vebt_member (?treeList ! h) l else False)
2 + ?n = Suc (Suc ?n)
?b \<le> ?a \<Longrightarrow> ?b + (?a - ?b) = ?a
vebt_mint (Node (Some (?mi, ?ma)) ?ux ?uy ?uz) = Some ?mi

goal (1 subgoal):
 1. vebt_member (Node (Some (mi, ma)) deg treeList summary) maxi
[PROOF STEP]
by (metis 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 mint_corr_help: "invar_vebt t n \<Longrightarrow> vebt_mint t = Some mini \<Longrightarrow> vebt_member t x \<Longrightarrow> mini \<le> x "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; vebt_mint t = Some mini; vebt_member t x\<rbrakk> \<Longrightarrow> mini \<le> x
[PROOF STEP]
by (smt VEBT_Member.vebt_member.simps(1) eq_iff option.inject less_imp_le_nat member_inv mi_ma_2_deg vebt_mint.elims of_nat_0 of_nat_0_le_iff of_nat_le_iff option.simps(3))


[STATEMENT]
lemma mint_corr_help_empty: "invar_vebt t n \<Longrightarrow> vebt_mint t = None \<Longrightarrow> set_vebt' t = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; vebt_mint t = None\<rbrakk> \<Longrightarrow> set_vebt' t = {}
[PROOF STEP]
by (metis VEBT_internal.maxt_corr_help_empty option.distinct(1) vebt_maxt.simps(1) vebt_maxt.simps(2) vebt_mint.elims)


[STATEMENT]
theorem mint_corr:assumes "invar_vebt t n" and "vebt_mint t = Some x" shows "min_in_set (set_vebt' t) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_in_set (set_vebt' t) x
[PROOF STEP]
using assms(1) assms(2) min_in_set_def mint_corr_help mint_member set_vebt'_def
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n
vebt_mint t = Some x
min_in_set ?xs ?x = (?x \<in> ?xs \<and> (\<forall>y\<in>?xs. ?x \<le> y))
\<lbrakk>invar_vebt ?t ?n; vebt_mint ?t = Some ?mini; vebt_member ?t ?x\<rbrakk> \<Longrightarrow> ?mini \<le> ?x
\<lbrakk>invar_vebt ?t ?n; vebt_mint ?t = Some ?maxi\<rbrakk> \<Longrightarrow> vebt_member ?t ?maxi
set_vebt' ?t = {x. vebt_member ?t x}

goal (1 subgoal):
 1. min_in_set (set_vebt' t) x
[PROOF STEP]
by auto


[STATEMENT]
theorem mint_sound:assumes "invar_vebt t n" and  "min_in_set (set_vebt' t) x" shows "vebt_mint t = Some x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_mint t = Some x
[PROOF STEP]
by (metis assms(1) assms(2) empty_Collect_eq eq_iff mem_Collect_eq min_in_set_def
 mint_corr_help mint_corr_help_empty mint_member option.exhaust set_vebt'_def)


[STATEMENT]
lemma summaxma:assumes "invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg" and "mi \<noteq> ma"
  shows "the (vebt_maxt summary) = high ma (deg div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg

goal (1 subgoal):
 1. the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
 2. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
case (4 n m)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set treeList. invar_vebt t n
invar_vebt summary m
length treeList = 2 ^ m
m = n
deg = n + m
\<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i
mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t))
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))

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
 2. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
have "both_member_options summary (high ma n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. both_member_options summary (high ma n)
[PROOF STEP]
using "4"(10) "4"(2) "4"(4) "4"(5) "4"(6) "4"(9) assms(2) deg_not_0 exp_split_high_low(1)
[PROOF STATE]
proof (prove)
using this:
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))
invar_vebt summary m
m = n
deg = n + m
\<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i
ma < 2 ^ deg
mi \<noteq> ma
invar_vebt ?t ?n \<Longrightarrow> 0 < ?n
\<lbrakk>?x < 2 ^ (?n + ?m); 0 < ?n; 0 < ?m\<rbrakk> \<Longrightarrow> high ?x ?n < 2 ^ ?m

goal (1 subgoal):
 1. both_member_options summary (high ma n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
both_member_options summary (high ma n)

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
 2. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
have "high ma n \<le> the (vebt_maxt summary)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high ma n \<le> the (vebt_maxt summary)
[PROOF STEP]
using  "4"(2) \<open>both_member_options summary
          (high ma n)\<close> empty_Collect_eq option.inject maxt_corr_help maxt_corr_help_empty
          not_None_eq set_vebt'_def valid_member_both_member_options
[PROOF STATE]
proof (prove)
using this:
invar_vebt summary m
both_member_options summary (high ma n)
({} = Collect ?P) = (\<forall>x. \<not> ?P x)
(Some ?x2.0 = Some ?y2.0) = (?x2.0 = ?y2.0)
\<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 = None\<rbrakk> \<Longrightarrow> set_vebt' ?t = {}
(?x \<noteq> None) = (\<exists>y. ?x = Some y)
set_vebt' ?t = {x. vebt_member ?t x}
\<lbrakk>invar_vebt ?t ?n; both_member_options ?t ?x\<rbrakk> \<Longrightarrow> vebt_member ?t ?x

goal (1 subgoal):
 1. high ma n \<le> the (vebt_maxt summary)
[PROOF STEP]
by (metis option.exhaust_sel)
[PROOF STATE]
proof (state)
this:
high ma n \<le> the (vebt_maxt summary)

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
 2. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
have "high ma n < the (vebt_maxt summary) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
assume "high ma n < the (vebt_maxt summary)"
[PROOF STATE]
proof (state)
this:
high ma n < the (vebt_maxt summary)

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
obtain maxs where "Some maxs = vebt_maxt summary"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>maxs. Some maxs = vebt_maxt summary \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis "4"(2) \<open>both_member_options summary (high ma n)\<close> empty_Collect_eq maxt_corr_help_empty
            not_None_eq set_vebt'_def valid_member_both_member_options)
[PROOF STATE]
proof (state)
this:
Some maxs = vebt_maxt summary

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "\<exists> x. both_member_options (treeList ! maxs) x"
[PROOF STATE]
proof (prove)
using this:
Some maxs = vebt_maxt summary

goal (1 subgoal):
 1. \<exists>x. both_member_options (treeList ! maxs) x
[PROOF STEP]
by (metis "4"(2) "4"(6) both_member_options_equiv_member maxt_member member_bound)
[PROOF STATE]
proof (state)
this:
\<exists>x. both_member_options (treeList ! maxs) x

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. both_member_options (treeList ! maxs) x
[PROOF STEP]
obtain x where "both_member_options (treeList ! maxs) x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. both_member_options (treeList ! maxs) x

goal (1 subgoal):
 1. (\<And>x. both_member_options (treeList ! maxs) x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
both_member_options (treeList ! maxs) x

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "vebt_member (treeList ! maxs) x"
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! maxs) x

goal (1 subgoal):
 1. vebt_member (treeList ! maxs) x
[PROOF STEP]
by (metis "4"(1) "4"(2) "4"(3) \<open>Some maxs = vebt_maxt summary\<close> maxt_member member_bound nth_mem valid_member_both_member_options)
[PROOF STATE]
proof (state)
this:
vebt_member (treeList ! maxs) x

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
have "maxs < 2^m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxs < 2 ^ m
[PROOF STEP]
by (metis "4"(2) \<open>Some maxs = vebt_maxt summary\<close> maxt_member member_bound)
[PROOF STATE]
proof (state)
this:
maxs < 2 ^ m

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
have "invar_vebt (treeList ! maxs) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar_vebt (treeList ! maxs) n
[PROOF STEP]
by (metis "4"(1) "4"(3) \<open>maxs < 2 ^ m\<close> inthall member_def)
[PROOF STATE]
proof (state)
this:
invar_vebt (treeList ! maxs) n

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "x < 2^n"
[PROOF STATE]
proof (prove)
using this:
invar_vebt (treeList ! maxs) n

goal (1 subgoal):
 1. x < 2 ^ n
[PROOF STEP]
using \<open>vebt_member (treeList ! maxs) x\<close> member_bound
[PROOF STATE]
proof (prove)
using this:
invar_vebt (treeList ! maxs) n
vebt_member (treeList ! maxs) x
\<lbrakk>vebt_member ?tree ?x; invar_vebt ?tree ?n\<rbrakk> \<Longrightarrow> ?x < 2 ^ ?n

goal (1 subgoal):
 1. x < 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < 2 ^ n

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
let ?X =  "2^n*maxs + x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
have "high ?X n = maxs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high (2 ^ n * maxs + x) n = maxs
[PROOF STEP]
by (simp add: \<open>x < 2 ^ n\<close> high_inv mult.commute)
[PROOF STATE]
proof (state)
this:
high (2 ^ n * maxs + x) n = maxs

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) (2^n*maxs + x)"
[PROOF STATE]
proof (prove)
using this:
high (2 ^ n * maxs + x) n = maxs

goal (1 subgoal):
 1. both_member_options (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)
[PROOF STEP]
by (metis "4"(3) "4"(4) "4"(5) One_nat_def Suc_leI \<open>both_member_options (treeList ! maxs) x\<close> \<open>maxs < 2 ^ m\<close> \<open>x < 2 ^ n\<close> add_self_div_2 assms(1) both_member_options_from_chilf_to_complete_tree deg_not_0 low_inv mult.commute)
[PROOF STATE]
proof (state)
this:
both_member_options (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "vebt_member (Node (Some (mi, ma)) deg treeList summary) ?X"
[PROOF STATE]
proof (prove)
using this:
both_member_options (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)

goal (1 subgoal):
 1. vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)
[PROOF STEP]
using assms(1) both_member_options_equiv_member
[PROOF STATE]
proof (prove)
using this:
both_member_options (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)
invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg
invar_vebt ?t ?n \<Longrightarrow> both_member_options ?t ?x = vebt_member ?t ?x

goal (1 subgoal):
 1. vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
have "high ?X n> high ma n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high ma n < high (2 ^ n * maxs + x) n
[PROOF STEP]
by (metis \<open>Some maxs = vebt_maxt summary\<close> \<open>high (2 ^ n * maxs + x) n = maxs\<close> \<open>high ma n < the (vebt_maxt summary)\<close> option.exhaust_sel option.inject option.simps(3))
[PROOF STATE]
proof (state)
this:
high ma n < high (2 ^ n * maxs + x) n

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "?X > ma"
[PROOF STATE]
proof (prove)
using this:
high ma n < high (2 ^ n * maxs + x) n

goal (1 subgoal):
 1. ma < 2 ^ n * maxs + x
[PROOF STEP]
by (metis div_le_mono high_def not_le)
[PROOF STATE]
proof (state)
this:
ma < 2 ^ n * maxs + x

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ma < 2 ^ n * maxs + x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ma < 2 ^ n * maxs + x

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis "4"(8) \<open>vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)\<close> leD member_inv not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
high ma n < the (vebt_maxt summary) \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
 2. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
high ma n < the (vebt_maxt summary) \<Longrightarrow> False

goal (1 subgoal):
 1. the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
using "4"(4) "4"(5) \<open>high ma n \<le> the (vebt_maxt summary)\<close>
[PROOF STATE]
proof (prove)
using this:
high ma n < the (vebt_maxt summary) \<Longrightarrow> False
m = n
deg = n + m
high ma n \<le> the (vebt_maxt summary)

goal (1 subgoal):
 1. the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
the (vebt_maxt summary) = high ma (deg div 2)

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
case (5 n m)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set treeList. invar_vebt t n
invar_vebt summary m
length treeList = 2 ^ m
m = Suc n
deg = n + m
\<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i
mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t))
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))

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
have "both_member_options summary (high ma n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. both_member_options summary (high ma n)
[PROOF STEP]
by (metis "5"(10) "5"(5) "5"(6) "5"(9) Euclidean_Division.div_eq_0_iff assms(2) div_exp_eq high_def nat.simps(3) numerals(2) power_not_zero)
[PROOF STATE]
proof (state)
this:
both_member_options summary (high ma n)

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
have "high ma n \<le> the (vebt_maxt summary)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high ma n \<le> the (vebt_maxt summary)
[PROOF STEP]
by (metis "5"(2) VEBT_Member.vebt_member.simps(2) \<open>both_member_options summary (high ma n)\<close> vebt_maxt.elims maxt_corr_help minNull.simps(1) min_Null_member option.exhaust_sel option.simps(3) valid_member_both_member_options)
[PROOF STATE]
proof (state)
this:
high ma n \<le> the (vebt_maxt summary)

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
have "high ma n < the (vebt_maxt summary) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
assume "high ma n < the (vebt_maxt summary)"
[PROOF STATE]
proof (state)
this:
high ma n < the (vebt_maxt summary)

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
obtain maxs where "Some maxs = vebt_maxt summary"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>maxs. Some maxs = vebt_maxt summary \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis "5"(2) \<open>both_member_options summary (high ma n)\<close> empty_Collect_eq maxt_corr_help_empty
         not_None_eq set_vebt'_def valid_member_both_member_options)
[PROOF STATE]
proof (state)
this:
Some maxs = vebt_maxt summary

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "\<exists> x. both_member_options (treeList ! maxs) x"
[PROOF STATE]
proof (prove)
using this:
Some maxs = vebt_maxt summary

goal (1 subgoal):
 1. \<exists>x. both_member_options (treeList ! maxs) x
[PROOF STEP]
by (metis "5"(2) "5"(6) both_member_options_equiv_member maxt_member member_bound)
[PROOF STATE]
proof (state)
this:
\<exists>x. both_member_options (treeList ! maxs) x

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. both_member_options (treeList ! maxs) x
[PROOF STEP]
obtain x where "both_member_options (treeList ! maxs) x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. both_member_options (treeList ! maxs) x

goal (1 subgoal):
 1. (\<And>x. both_member_options (treeList ! maxs) x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
both_member_options (treeList ! maxs) x

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "vebt_member (treeList ! maxs) x"
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! maxs) x

goal (1 subgoal):
 1. vebt_member (treeList ! maxs) x
[PROOF STEP]
by (metis "5"(1) "5"(2) "5"(3) \<open>Some maxs = vebt_maxt summary\<close> both_member_options_equiv_member maxt_member member_bound nth_mem)
[PROOF STATE]
proof (state)
this:
vebt_member (treeList ! maxs) x

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
have "maxs < 2^m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxs < 2 ^ m
[PROOF STEP]
by (metis "5"(2) \<open>Some maxs = vebt_maxt summary\<close> maxt_member member_bound)
[PROOF STATE]
proof (state)
this:
maxs < 2 ^ m

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
have "invar_vebt (treeList ! maxs) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar_vebt (treeList ! maxs) n
[PROOF STEP]
by (metis "5"(1) "5"(3) \<open>maxs < 2 ^ m\<close> inthall member_def)
[PROOF STATE]
proof (state)
this:
invar_vebt (treeList ! maxs) n

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "x < 2^n"
[PROOF STATE]
proof (prove)
using this:
invar_vebt (treeList ! maxs) n

goal (1 subgoal):
 1. x < 2 ^ n
[PROOF STEP]
using \<open>vebt_member (treeList ! maxs) x\<close> member_bound
[PROOF STATE]
proof (prove)
using this:
invar_vebt (treeList ! maxs) n
vebt_member (treeList ! maxs) x
\<lbrakk>vebt_member ?tree ?x; invar_vebt ?tree ?n\<rbrakk> \<Longrightarrow> ?x < 2 ^ ?n

goal (1 subgoal):
 1. x < 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < 2 ^ n

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
let ?X =  "2^n*maxs + x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
have "high ?X n = maxs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high (2 ^ n * maxs + x) n = maxs
[PROOF STEP]
by (simp add: \<open>x < 2 ^ n\<close> high_inv mult.commute)
[PROOF STATE]
proof (state)
this:
high (2 ^ n * maxs + x) n = maxs

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) (2^n*maxs + x)"
[PROOF STATE]
proof (prove)
using this:
high (2 ^ n * maxs + x) n = maxs

goal (1 subgoal):
 1. both_member_options (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)
[PROOF STEP]
by (smt (z3) "5"(3) "5"(4) "5"(5) \<open>both_member_options (treeList ! maxs) x\<close> \<open>maxs < 2 ^ m\<close> \<open>x < 2 ^ n\<close> add_Suc_right add_self_div_2 both_member_options_from_chilf_to_complete_tree even_Suc_div_two le_add1 low_inv mult.commute odd_add plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
both_member_options (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "vebt_member (Node (Some (mi, ma)) deg treeList summary) ?X"
[PROOF STATE]
proof (prove)
using this:
both_member_options (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)

goal (1 subgoal):
 1. vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)
[PROOF STEP]
using assms(1) both_member_options_equiv_member
[PROOF STATE]
proof (prove)
using this:
both_member_options (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)
invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg
invar_vebt ?t ?n \<Longrightarrow> both_member_options ?t ?x = vebt_member ?t ?x

goal (1 subgoal):
 1. vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
have "high ?X n> high ma n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high ma n < high (2 ^ n * maxs + x) n
[PROOF STEP]
by (metis \<open>Some maxs = vebt_maxt summary\<close> \<open>high (2 ^ n * maxs + x) n = maxs\<close> \<open>high ma n < the (vebt_maxt summary)\<close> option.sel)
[PROOF STATE]
proof (state)
this:
high ma n < high (2 ^ n * maxs + x) n

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
hence "?X > ma"
[PROOF STATE]
proof (prove)
using this:
high ma n < high (2 ^ n * maxs + x) n

goal (1 subgoal):
 1. ma < 2 ^ n * maxs + x
[PROOF STEP]
by (metis div_le_mono high_def not_le)
[PROOF STATE]
proof (state)
this:
ma < 2 ^ n * maxs + x

goal (1 subgoal):
 1. high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ma < 2 ^ n * maxs + x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ma < 2 ^ n * maxs + x

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis "5"(8) \<open>vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)\<close> leD member_inv not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
high ma n < the (vebt_maxt summary) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<forall>t\<in>set treeList. invar_vebt t n; invar_vebt summary m; length treeList = 2 ^ m; m = Suc n; deg = n + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); 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))\<rbrakk> \<Longrightarrow> the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
high ma n < the (vebt_maxt summary) \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
high ma n < the (vebt_maxt summary) \<Longrightarrow> False

goal (1 subgoal):
 1. the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
using "5"(4) "5"(5) \<open>high ma n \<le> the(vebt_maxt summary)\<close>
[PROOF STATE]
proof (prove)
using this:
high ma n < the (vebt_maxt summary) \<Longrightarrow> False
m = Suc n
deg = n + m
high ma n \<le> the (vebt_maxt summary)

goal (1 subgoal):
 1. the (vebt_maxt summary) = high ma (deg div 2)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
the (vebt_maxt summary) = high ma (deg div 2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
the (vebt_maxt summary) = high ma (deg div 2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maxbmo: "vebt_maxt t = Some x \<Longrightarrow> both_member_options t x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_maxt t = Some x \<Longrightarrow> both_member_options t x
[PROOF STEP]
apply(induction t rule: vebt_maxt.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. vebt_maxt (Leaf a b) = Some x \<Longrightarrow> both_member_options (Leaf a b) x
 2. \<And>uu_ uv_ uw_. vebt_maxt (Node None uu_ uv_ uw_) = Some x \<Longrightarrow> both_member_options (Node None uu_ uv_ uw_) x
 3. \<And>mi ma ux_ uy_ uz_. vebt_maxt (Node (Some (mi, ma)) ux_ uy_ uz_) = Some x \<Longrightarrow> both_member_options (Node (Some (mi, ma)) ux_ uy_ uz_) x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. (if b then Some 1 else if a then Some 0 else None) = Some x \<Longrightarrow> both_member_options (Leaf a b) x
 2. \<And>mi ux_ uy_ uz_. both_member_options (Node (Some (mi, x)) ux_ uy_ uz_) x
[PROOF STEP]
apply (metis both_member_options_def naive_member.simps(1) option.distinct(1) option.sel zero_neq_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mi ux_ uy_ uz_. both_member_options (Node (Some (mi, x)) ux_ uy_ uz_) x
[PROOF STEP]
by (metis One_nat_def Suc_le_D both_member_options_def div_by_1 div_greater_zero_iff membermima.simps(3) membermima.simps(4) not_gr0)


[STATEMENT]
lemma misiz:"invar_vebt t n \<Longrightarrow> Some m = vebt_mint t \<Longrightarrow> m < 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; Some m = vebt_mint t\<rbrakk> \<Longrightarrow> m < 2 ^ n
[PROOF STEP]
by (metis member_bound mint_member)