[STATEMENT]
lemma mintlistlength: assumes "invar_vebt (Node (Some (mi, ma)) deg treeList summary) n " "
    mi \<noteq> ma " shows " ma > mi \<and> (\<exists> m. Some m = vebt_mint summary \<and> m < 2^(n - n div 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n

goal (1 subgoal):
 1. mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
case (4 n m)
[PROOF STATE]
proof (state)
this:
n = deg
\<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>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
hence "both_member_options (treeList ! high ma n) (low ma n)"
[PROOF STATE]
proof (prove)
using this:
n = deg
\<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 (1 subgoal):
 1. both_member_options (treeList ! high ma n) (low ma n)
[PROOF STEP]
by (metis assms(2) high_bound_aux)
[PROOF STATE]
proof (state)
this:
both_member_options (treeList ! high ma n) (low ma n)

goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
both_member_options (treeList ! high ma n) (low ma n)

goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
hence "both_member_options summary (high ma n)"
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! high ma n) (low ma n)

goal (1 subgoal):
 1. both_member_options summary (high ma n)
[PROOF STEP]
using "4"(10) "4"(6) "4"(7) high_bound_aux
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! high ma n) (low ma n)
ma < 2 ^ deg
deg = n + m
\<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i
?ma < 2 ^ (?n + ?m) \<Longrightarrow> high ?ma ?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>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
both_member_options summary (high ma n)

goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
both_member_options summary (high ma n)
[PROOF STEP]
obtain mini where "Some mini = vebt_mint summary"
[PROOF STATE]
proof (prove)
using this:
both_member_options summary (high ma n)

goal (1 subgoal):
 1. (\<And>mini. Some mini = vebt_mint summary \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis "4"(3) empty_Collect_eq mint_corr_help_empty option.exhaust_sel set_vebt'_def valid_member_both_member_options)
[PROOF STATE]
proof (state)
this:
Some mini = vebt_mint summary

goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Some mini = vebt_mint summary

goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
hence "mini < 2^m"
[PROOF STATE]
proof (prove)
using this:
Some mini = vebt_mint summary

goal (1 subgoal):
 1. mini < 2 ^ m
[PROOF STEP]
by (metis "4"(3)  mint_member member_bound)
[PROOF STATE]
proof (state)
this:
mini < 2 ^ m

goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mini < 2 ^ m

goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
have "m = (deg - deg div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = deg - deg div 2
[PROOF STEP]
using 4(6) 4(5)
[PROOF STATE]
proof (prove)
using this:
deg = n + m
m = n

goal (1 subgoal):
 1. m = deg - deg div 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = deg - deg div 2

goal (2 subgoals):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
 2. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
both_member_options (treeList ! high ma n) (low ma n)
both_member_options summary (high ma n)
Some mini = vebt_mint summary
mini < 2 ^ m
m = deg - deg div 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! high ma n) (low ma n)
both_member_options summary (high ma n)
Some mini = vebt_mint summary
mini < 2 ^ m
m = deg - deg div 2

goal (1 subgoal):
 1. mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
using 4(1) assms 4(9)
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! high ma n) (low ma n)
both_member_options summary (high ma n)
Some mini = vebt_mint summary
mini < 2 ^ m
m = deg - deg div 2
n = deg
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n
mi \<noteq> ma
mi \<le> ma

goal (1 subgoal):
 1. mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
case (5 n m)
[PROOF STATE]
proof (state)
this:
n = deg
\<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>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
hence "both_member_options (treeList ! high ma n) (low ma n)"
[PROOF STATE]
proof (prove)
using this:
n = deg
\<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. both_member_options (treeList ! high ma n) (low ma n)
[PROOF STEP]
by (metis assms(2) high_bound_aux)
[PROOF STATE]
proof (state)
this:
both_member_options (treeList ! high ma n) (low ma n)

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
both_member_options (treeList ! high ma n) (low ma n)

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
hence "both_member_options summary (high ma n)"
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! high ma n) (low ma n)

goal (1 subgoal):
 1. both_member_options summary (high ma n)
[PROOF STEP]
using "5"(10) "5"(6) "5"(7) high_bound_aux
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! high ma n) (low ma n)
ma < 2 ^ deg
deg = n + m
\<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i
?ma < 2 ^ (?n + ?m) \<Longrightarrow> high ?ma ?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 (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
both_member_options summary (high ma n)

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
both_member_options summary (high ma n)
[PROOF STEP]
obtain mini where "Some mini = vebt_mint summary"
[PROOF STATE]
proof (prove)
using this:
both_member_options summary (high ma n)

goal (1 subgoal):
 1. (\<And>mini. Some mini = vebt_mint summary \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis "5"(3) empty_Collect_eq mint_corr_help_empty option.exhaust_sel set_vebt'_def valid_member_both_member_options)
[PROOF STATE]
proof (state)
this:
Some mini = vebt_mint summary

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Some mini = vebt_mint summary

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
hence "mini < 2^m"
[PROOF STATE]
proof (prove)
using this:
Some mini = vebt_mint summary

goal (1 subgoal):
 1. mini < 2 ^ m
[PROOF STEP]
by (metis "5"(3)  mint_member member_bound)
[PROOF STATE]
proof (state)
this:
mini < 2 ^ m

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mini < 2 ^ m

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
have "m = (deg - deg div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = deg - deg div 2
[PROOF STEP]
using 5(6) 5(5)
[PROOF STATE]
proof (prove)
using this:
deg = n + m
m = Suc n

goal (1 subgoal):
 1. m = deg - deg div 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = deg - deg div 2

goal (1 subgoal):
 1. \<And>na m. \<lbrakk>n = deg; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; deg = na + 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 na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
both_member_options (treeList ! high ma n) (low ma n)
both_member_options summary (high ma n)
Some mini = vebt_mint summary
mini < 2 ^ m
m = deg - deg div 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! high ma n) (low ma n)
both_member_options summary (high ma n)
Some mini = vebt_mint summary
mini < 2 ^ m
m = deg - deg div 2

goal (1 subgoal):
 1. mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
using 5(1) assms 5(9)
[PROOF STATE]
proof (prove)
using this:
both_member_options (treeList ! high ma n) (low ma n)
both_member_options summary (high ma n)
Some mini = vebt_mint summary
mini < 2 ^ m
m = deg - deg div 2
n = deg
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n
mi \<noteq> ma
mi \<le> ma

goal (1 subgoal):
 1. mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mi < ma \<and> (\<exists>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_minus_is_div:
  "b \<le> a \<Longrightarrow> (2 :: nat) ^ (a - b) = 2 ^ a div 2 ^ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b
[PROOF STEP]
apply (induct a arbitrary: b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. b \<le> 0 \<Longrightarrow> 2 ^ (0 - b) = 2 ^ 0 div 2 ^ b
 2. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b \<le> Suc a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b \<le> Suc a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b
[PROOF STEP]
apply (erule le_SucE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b \<le> a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b
 2. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b = Suc a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b
[PROOF STEP]
apply (clarsimp simp:Suc_diff_le le_iff_add power_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b = Suc a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nested_mint:assumes "invar_vebt (Node (Some (mi, ma)) deg treeList summary) n " "n = Suc (Suc va) ""
    \<not> ma < mi "" ma \<noteq> mi " shows "
    high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2))
    < length treeList"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
have setprop: "t \<in> set treeList \<Longrightarrow> invar_vebt t (n div 2 )" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> set treeList \<Longrightarrow> invar_vebt t (n div 2)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n

goal (1 subgoal):
 1. t \<in> set treeList \<Longrightarrow> invar_vebt t (n div 2)
[PROOF STEP]
by (cases) simp+
[PROOF STATE]
proof (state)
this:
?t \<in> set treeList \<Longrightarrow> invar_vebt ?t (n div 2)

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
have listlength: "length treeList = 2^(n - n div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length treeList = 2 ^ (n - n div 2)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n

goal (1 subgoal):
 1. length treeList = 2 ^ (n - n div 2)
[PROOF STEP]
by (cases) simp+
[PROOF STATE]
proof (state)
this:
length treeList = 2 ^ (n - n div 2)

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
have sumprop: "invar_vebt summary (n - n div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar_vebt summary (n - n div 2)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n

goal (1 subgoal):
 1. invar_vebt summary (n - n div 2)
[PROOF STEP]
by (cases) simp+
[PROOF STATE]
proof (state)
this:
invar_vebt summary (n - n div 2)

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
have mimaxprop: "mi \<le> ma \<and> ma \<le> 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mi \<le> ma \<and> ma \<le> 2 ^ n
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n

goal (1 subgoal):
 1. mi \<le> ma \<and> ma \<le> 2 ^ n
[PROOF STEP]
by cases  simp+
[PROOF STATE]
proof (state)
this:
mi \<le> ma \<and> ma \<le> 2 ^ n

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
hence xbound: "mi \<le> x \<Longrightarrow> x \<le> ma \<Longrightarrow> high x (n div 2) \<le> length treeList " for x
[PROOF STATE]
proof (prove)
using this:
mi \<le> ma \<and> ma \<le> 2 ^ n

goal (1 subgoal):
 1. \<lbrakk>mi \<le> x; x \<le> ma\<rbrakk> \<Longrightarrow> high x (n div 2) \<le> length treeList
[PROOF STEP]
using div_le_dividend div_le_mono high_def listlength power_minus_is_div
[PROOF STATE]
proof (prove)
using this:
mi \<le> ma \<and> ma \<le> 2 ^ n
?m div ?n \<le> ?m
?m \<le> ?n \<Longrightarrow> ?m div ?k \<le> ?n div ?k
high ?x ?n = ?x div 2 ^ ?n
length treeList = 2 ^ (n - n div 2)
?b \<le> ?a \<Longrightarrow> 2 ^ (?a - ?b) = 2 ^ ?a div 2 ^ ?b

goal (1 subgoal):
 1. \<lbrakk>mi \<le> x; x \<le> ma\<rbrakk> \<Longrightarrow> high x (n div 2) \<le> length treeList
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>mi \<le> ?x; ?x \<le> ma\<rbrakk> \<Longrightarrow> high ?x (n div 2) \<le> length treeList

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
have contcong:"i < length treeList \<Longrightarrow> \<exists> x. both_member_options (treeList ! i) x \<longleftrightarrow> both_member_options summary i " for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length treeList \<Longrightarrow> \<exists>x. both_member_options (treeList ! i) x = both_member_options summary i
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n

goal (1 subgoal):
 1. i < length treeList \<Longrightarrow> \<exists>x. both_member_options (treeList ! i) x = both_member_options summary i
[PROOF STEP]
by cases  auto+
[PROOF STATE]
proof (state)
this:
?i < length treeList \<Longrightarrow> \<exists>x. both_member_options (treeList ! ?i) x = both_member_options summary ?i

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
obtain m where " Some m = vebt_mint summary \<and> m < 2^(n - n div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) assms(4) mintlistlength
[PROOF STATE]
proof (prove)
using this:
invar_vebt (Node (Some (mi, ma)) deg treeList summary) n
ma \<noteq> mi
\<lbrakk>invar_vebt (Node (Some (?mi, ?ma)) ?deg ?treeList ?summary) ?n; ?mi \<noteq> ?ma\<rbrakk> \<Longrightarrow> ?mi < ?ma \<and> (\<exists>m. Some m = vebt_mint ?summary \<and> m < 2 ^ (?n - ?n div 2))

goal (1 subgoal):
 1. (\<And>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2)

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2)
[PROOF STEP]
obtain miny where "(vebt_mint (treeList ! the (vebt_mint summary))) =Some miny"
[PROOF STATE]
proof (prove)
using this:
Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2)

goal (1 subgoal):
 1. (\<And>miny. vebt_mint (treeList ! the (vebt_mint summary)) = Some miny \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis both_member_options_equiv_member contcong empty_Collect_eq listlength mint_corr_help_empty mint_member nth_mem option.exhaust_sel option.sel setprop sumprop set_vebt'_def)
[PROOF STATE]
proof (state)
this:
vebt_mint (treeList ! the (vebt_mint summary)) = Some miny

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
hence "miny < 2^(n div 2)"
[PROOF STATE]
proof (prove)
using this:
vebt_mint (treeList ! the (vebt_mint summary)) = Some miny

goal (1 subgoal):
 1. miny < 2 ^ (n div 2)
[PROOF STEP]
by (metis \<open>\<And>thesis. (\<And>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2) \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> listlength misiz nth_mem option.sel setprop)
[PROOF STATE]
proof (state)
this:
miny < 2 ^ (n div 2)

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
miny < 2 ^ (n div 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
miny < 2 ^ (n div 2)

goal (1 subgoal):
 1. high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList
[PROOF STEP]
by (metis \<open>\<And>thesis. (\<And>m. Some m = vebt_mint summary \<and> m < 2 ^ (n - n div 2) \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \<open>vebt_mint (treeList ! the (vebt_mint summary)) = Some miny\<close> assms(2) div2_Suc_Suc high_inv listlength option.sel power_Suc)
[PROOF STATE]
proof (state)
this:
high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minminNull: "vebt_mint t = None \<Longrightarrow> minNull t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_mint t = None \<Longrightarrow> minNull t
[PROOF STEP]
by (metis minNull.simps(1) minNull.simps(4) vebt_mint.elims option.distinct(1))


[STATEMENT]
lemma minNullmin: "minNull t \<Longrightarrow> vebt_mint t = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minNull t \<Longrightarrow> vebt_mint t = None
[PROOF STEP]
by (metis minNull.elims(2) vebt_mint.simps(1) vebt_mint.simps(2))


[STATEMENT]
lemma decide_sent_msgs_threshold:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nvp: "decide (rho r p) \<noteq> Some v"
  and vp: "decide (rho (Suc r) p) = Some v"
  shows "card {qq. sendMsg Ate_M r qq p (rho r qq) = v} > E - \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>p
    where mu: "\<mu>p \<in> SHOmsgVectors Ate_M r p (rho r) (HOs r p) (SHOs r p)"
      and nxt: "nextState Ate_M r p (rho r p) \<mu>p (rho (Suc r) p)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<And>\<mu>p. \<lbrakk>\<mu>p \<in> SHOmsgVectors Ate_M r p (rho r) (HOs r p) (SHOs r p); nextState Ate_M r p (rho r p) \<mu>p (rho (Suc r) p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
\<mu>p \<in> SHOmsgVectors Ate_M r p (rho r) (HOs r p) (SHOs r p)
nextState Ate_M r p (rho r p) \<mu>p (rho (Suc r) p)

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
from mu
[PROOF STATE]
proof (chain)
picking this:
\<mu>p \<in> SHOmsgVectors Ate_M r p (rho r) (HOs r p) (SHOs r p)
[PROOF STEP]
have "{qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p)
          \<subseteq> {qq. sendMsg Ate_M r qq p (rho r qq) = v}"
       (is "?vrcvdp - ?ahop \<subseteq> ?vsentp")
[PROOF STATE]
proof (prove)
using this:
\<mu>p \<in> SHOmsgVectors Ate_M r p (rho r) (HOs r p) (SHOs r p)

goal (1 subgoal):
 1. {qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p) \<subseteq> {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
by (auto simp: SHOmsgVectors_def)
[PROOF STATE]
proof (state)
this:
{qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p) \<subseteq> {qq. sendMsg Ate_M r qq p (rho r qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
hence "card (?vrcvdp - ?ahop) \<le> card ?vsentp"
    and "card (?vrcvdp - ?ahop) \<ge> card ?vrcvdp - card ?ahop"
[PROOF STATE]
proof (prove)
using this:
{qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p) \<subseteq> {qq. sendMsg Ate_M r qq p (rho r qq) = v}

goal (1 subgoal):
 1. card ({qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p)) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v} &&& card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card ({qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p))
[PROOF STEP]
by (auto simp: card_mono diff_card_le_card_Diff)
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p)) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card ({qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p))

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
hence "card ?vsentp \<ge> card ?vrcvdp - card ?ahop"
[PROOF STATE]
proof (prove)
using this:
card ({qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p)) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card ({qq. \<mu>p qq = Some v} - (HOs r p - SHOs r p))

goal (1 subgoal):
 1. card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
from nxt nvp vp
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M r p (rho r p) \<mu>p (rho (Suc r) p)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v
[PROOF STEP]
have "card ?vrcvdp > E"
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M r p (rho r p) \<mu>p (rho (Suc r) p)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v

goal (1 subgoal):
 1. E < card {qq. \<mu>p qq = Some v}
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
[PROOF STATE]
proof (state)
this:
E < card {qq. \<mu>p qq = Some v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
E < card {qq. \<mu>p qq = Some v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
from comm
[PROOF STATE]
proof (chain)
picking this:
SHOcommPerRd Ate_M (HOs r) (SHOs r)
[PROOF STEP]
have "card (HOs r p - SHOs r p) \<le> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs r) (SHOs r)

goal (1 subgoal):
 1. card (HOs r p - SHOs r p) \<le> \<alpha>
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_commPerRd_def)
[PROOF STATE]
proof (state)
this:
card (HOs r p - SHOs r p) \<le> \<alpha>

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
E < card {qq. \<mu>p qq = Some v}
card (HOs r p - SHOs r p) \<le> \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
E < card {qq. \<mu>p qq = Some v}
card (HOs r p - SHOs r p) \<le> \<alpha>

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
using Egta
[PROOF STATE]
proof (prove)
using this:
card {qq. \<mu>p qq = Some v} - card (HOs r p - SHOs r p) \<le> card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
E < card {qq. \<mu>p qq = Some v}
card (HOs r p - SHOs r p) \<le> \<alpha>
\<alpha> < E

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma other_values_received:
  assumes comm: "SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nxt: "nextState Ate_M r q (rho r q) \<mu>q ((rho (Suc r)) q)"
  and muq: "\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)"
  and vsent: "card {qq. sendMsg Ate_M r qq q (rho r qq) = v} > E - \<alpha>"
             (is "card ?vsent > _")
  shows "card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2*\<alpha> - E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
from nxt muq
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M r q (rho r q) \<mu>q (rho (Suc r) q)
\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)
[PROOF STEP]
have "({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) - (HOs r q - SHOs r q)
        \<subseteq>  {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}"
    (is "?notvrcvd - ?aho \<subseteq> ?notvsent")
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M r q (rho r q) \<mu>q (rho (Suc r) q)
\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)

goal (1 subgoal):
 1. {qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q) \<subseteq> {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}
[PROOF STEP]
unfolding SHOmsgVectors_def
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M r q (rho r q) \<mu>q (rho (Suc r) q)
\<mu>q \<in> {\<mu>. (\<forall>qa. (qa \<in> HOs r q) = (\<mu> qa \<noteq> None)) \<and> (\<forall>qa. qa \<in> SHOs r q \<inter> HOs r q \<longrightarrow> \<mu> qa = Some (sendMsg Ate_M r qa q (rho r qa)))}

goal (1 subgoal):
 1. {qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q) \<subseteq> {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q) \<subseteq> {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
hence "card ?notvsent \<ge> card (?notvrcvd - ?aho)"
    and "card (?notvrcvd - ?aho) \<ge> card ?notvrcvd - card ?aho"
[PROOF STATE]
proof (prove)
using this:
{qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q) \<subseteq> {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q)) \<le> card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} &&& card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) - card (HOs r q - SHOs r q) \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q))
[PROOF STEP]
by (auto simp: card_mono diff_card_le_card_Diff)
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q)) \<le> card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) - card (HOs r q - SHOs r q) \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q))

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q)) \<le> card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) - card (HOs r q - SHOs r q) \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q))

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
from comm
[PROOF STATE]
proof (chain)
picking this:
SHOcommPerRd Ate_M (HOs r) (SHOs r)
[PROOF STEP]
have "card ?aho \<le> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs r) (SHOs r)

goal (1 subgoal):
 1. card (HOs r q - SHOs r q) \<le> \<alpha>
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_commPerRd_def)
[PROOF STATE]
proof (state)
this:
card (HOs r q - SHOs r q) \<le> \<alpha>

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (HOs r q - SHOs r q) \<le> \<alpha>

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
have 1: "card ?notvsent + card ?vsent = card (?notvsent \<union> ?vsent)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = v} = card ({qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v})
[PROOF STEP]
by (subst card_Un_Int) auto
[PROOF STATE]
proof (state)
this:
card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = v} = card ({qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v})

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
have "?notvsent \<union> ?vsent = (UNIV::Proc set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v} = UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v} = UNIV

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
hence "card (?notvsent \<union> ?vsent) = N"
[PROOF STATE]
proof (prove)
using this:
{qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v} = UNIV

goal (1 subgoal):
 1. card ({qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v}) = N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card ({qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v}) = N

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
with 1 vsent
[PROOF STATE]
proof (chain)
picking this:
card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = v} = card ({qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v})
E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = v}
card ({qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v}) = N
[PROOF STEP]
have "card ?notvsent \<le>  N - (E + 1 - \<alpha>)"
[PROOF STATE]
proof (prove)
using this:
card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = v} = card ({qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v})
E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = v}
card ({qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = v}) = N

goal (1 subgoal):
 1. card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<le> N - (E + 1 - \<alpha>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<le> N - (E + 1 - \<alpha>)

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q)) \<le> card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) - card (HOs r q - SHOs r q) \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q))
card (HOs r q - SHOs r q) \<le> \<alpha>
card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<le> N - (E + 1 - \<alpha>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q)) \<le> card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) - card (HOs r q - SHOs r q) \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q))
card (HOs r q - SHOs r q) \<le> \<alpha>
card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<le> N - (E + 1 - \<alpha>)

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
using EltN Egta
[PROOF STATE]
proof (prove)
using this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q)) \<le> card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v}
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) - card (HOs r q - SHOs r q) \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q - (HOs r q - SHOs r q))
card (HOs r q - SHOs r q) \<le> \<alpha>
card {qq. sendMsg Ate_M r qq q (rho r qq) \<noteq> v} \<le> N - (E + 1 - \<alpha>)
E < N
\<alpha> < E

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mostOftenRcvd_v:
  assumes comm: "SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nxt: "nextState Ate_M r q (rho r q) \<mu>q ((rho (Suc r)) q)"
  and muq: "\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)"
  and threshold_T: "card {qq. \<mu>q qq \<noteq> None} > T"
  and threshold_E: "card {qq. sendMsg Ate_M r qq q (rho r qq) = v} > E - \<alpha>"
  shows "mostOftenRcvd \<mu>q = {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
from muq
[PROOF STATE]
proof (chain)
picking this:
\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)
[PROOF STEP]
have hodef:"HOs r q = {qq. \<mu>q qq \<noteq> None}"
[PROOF STATE]
proof (prove)
using this:
\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)

goal (1 subgoal):
 1. HOs r q = {qq. \<mu>q qq \<noteq> None}
[PROOF STEP]
unfolding SHOmsgVectors_def
[PROOF STATE]
proof (prove)
using this:
\<mu>q \<in> {\<mu>. (\<forall>qa. (qa \<in> HOs r q) = (\<mu> qa \<noteq> None)) \<and> (\<forall>qa. qa \<in> SHOs r q \<inter> HOs r q \<longrightarrow> \<mu> qa = Some (sendMsg Ate_M r qa q (rho r qa)))}

goal (1 subgoal):
 1. HOs r q = {qq. \<mu>q qq \<noteq> None}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HOs r q = {qq. \<mu>q qq \<noteq> None}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
from comm nxt muq threshold_E
[PROOF STATE]
proof (chain)
picking this:
SHOcommPerRd Ate_M (HOs r) (SHOs r)
nextState Ate_M r q (rho r q) \<mu>q (rho (Suc r) q)
\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)
E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = v}
[PROOF STEP]
have "card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2*\<alpha> - E"
    (is "card ?heardnotv \<le> _")
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs r) (SHOs r)
nextState Ate_M r q (rho r q) \<mu>q (rho (Suc r) q)
\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)
E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = v}

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
[PROOF STEP]
by (rule other_values_received)
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
have "card ?heardnotv \<ge> T + 1 - card {qq. \<mu>q qq = Some v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
[PROOF STEP]
from muq
[PROOF STATE]
proof (chain)
picking this:
\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)
[PROOF STEP]
have "?heardnotv = (HOs r q) - {qq. \<mu>q qq = Some v}"
      and "{qq. \<mu>q qq = Some v} \<subseteq> HOs r q"
[PROOF STATE]
proof (prove)
using this:
\<mu>q \<in> SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)

goal (1 subgoal):
 1. {qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q = HOs r q - {qq. \<mu>q qq = Some v} &&& {qq. \<mu>q qq = Some v} \<subseteq> HOs r q
[PROOF STEP]
unfolding SHOmsgVectors_def
[PROOF STATE]
proof (prove)
using this:
\<mu>q \<in> {\<mu>. (\<forall>qa. (qa \<in> HOs r q) = (\<mu> qa \<noteq> None)) \<and> (\<forall>qa. qa \<in> SHOs r q \<inter> HOs r q \<longrightarrow> \<mu> qa = Some (sendMsg Ate_M r qa q (rho r qa)))}

goal (1 subgoal):
 1. {qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q = HOs r q - {qq. \<mu>q qq = Some v} &&& {qq. \<mu>q qq = Some v} \<subseteq> HOs r q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q = HOs r q - {qq. \<mu>q qq = Some v}
{qq. \<mu>q qq = Some v} \<subseteq> HOs r q

goal (1 subgoal):
 1. T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
[PROOF STEP]
hence "card ?heardnotv = card (HOs r q) - card {qq. \<mu>q qq = Some v}"
[PROOF STATE]
proof (prove)
using this:
{qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q = HOs r q - {qq. \<mu>q qq = Some v}
{qq. \<mu>q qq = Some v} \<subseteq> HOs r q

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) = card (HOs r q) - card {qq. \<mu>q qq = Some v}
[PROOF STEP]
by (auto simp: card_Diff_subset)
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) = card (HOs r q) - card {qq. \<mu>q qq = Some v}

goal (1 subgoal):
 1. T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
[PROOF STEP]
with hodef threshold_T
[PROOF STATE]
proof (chain)
picking this:
HOs r q = {qq. \<mu>q qq \<noteq> None}
T < card {qq. \<mu>q qq \<noteq> None}
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) = card (HOs r q) - card {qq. \<mu>q qq = Some v}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HOs r q = {qq. \<mu>q qq \<noteq> None}
T < card {qq. \<mu>q qq \<noteq> None}
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) = card (HOs r q) - card {qq. \<mu>q qq = Some v}

goal (1 subgoal):
 1. T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
[PROOF STEP]
have "card {qq. \<mu>q qq = Some v} > card ?heardnotv"
[PROOF STATE]
proof (prove)
using this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) < card {qq. \<mu>q qq = Some v}
[PROOF STEP]
using TNaE
[PROOF STATE]
proof (prove)
using this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) \<le> N + 2 * \<alpha> - E
T + 1 - card {qq. \<mu>q qq = Some v} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
2 * (N + 2 * \<alpha> - E) \<le> T

goal (1 subgoal):
 1. card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) < card {qq. \<mu>q qq = Some v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) < card {qq. \<mu>q qq = Some v}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) < card {qq. \<mu>q qq = Some v}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) < card {qq. \<mu>q qq = Some v}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
assume w: "w \<noteq> v"
[PROOF STATE]
proof (state)
this:
w \<noteq> v

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
with hodef
[PROOF STATE]
proof (chain)
picking this:
HOs r q = {qq. \<mu>q qq \<noteq> None}
w \<noteq> v
[PROOF STEP]
have "{qq. \<mu>q qq = Some w} \<subseteq> ?heardnotv"
[PROOF STATE]
proof (prove)
using this:
HOs r q = {qq. \<mu>q qq \<noteq> None}
w \<noteq> v

goal (1 subgoal):
 1. {qq. \<mu>q qq = Some w} \<subseteq> {qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{qq. \<mu>q qq = Some w} \<subseteq> {qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
hence "card {qq. \<mu>q qq = Some w} \<le> card ?heardnotv"
[PROOF STATE]
proof (prove)
using this:
{qq. \<mu>q qq = Some w} \<subseteq> {qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q

goal (1 subgoal):
 1. card {qq. \<mu>q qq = Some w} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
[PROOF STEP]
by (auto simp: card_mono)
[PROOF STATE]
proof (state)
this:
card {qq. \<mu>q qq = Some w} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?w7 \<noteq> v \<Longrightarrow> card {qq. \<mu>q qq = Some ?w7} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) < card {qq. \<mu>q qq = Some v}
?w7 \<noteq> v \<Longrightarrow> card {qq. \<mu>q qq = Some ?w7} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)
[PROOF STEP]
have "{w. card {qq. \<mu>q qq = Some w} \<ge> card {qq. \<mu>q qq = Some v}} = {v}"
[PROOF STATE]
proof (prove)
using this:
card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q) < card {qq. \<mu>q qq = Some v}
?w7 \<noteq> v \<Longrightarrow> card {qq. \<mu>q qq = Some ?w7} \<le> card ({qq. \<mu>q qq \<noteq> Some v} \<inter> HOs r q)

goal (1 subgoal):
 1. {w. card {qq. \<mu>q qq = Some v} \<le> card {qq. \<mu>q qq = Some w}} = {v}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{w. card {qq. \<mu>q qq = Some v} \<le> card {qq. \<mu>q qq = Some w}} = {v}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{w. card {qq. \<mu>q qq = Some v} \<le> card {qq. \<mu>q qq = Some w}} = {v}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
unfolding mostOftenRcvd_def
[PROOF STATE]
proof (prove)
using this:
{w. card {qq. \<mu>q qq = Some v} \<le> card {qq. \<mu>q qq = Some w}} = {v}

goal (1 subgoal):
 1. {v. \<forall>w. card {qq. \<mu>q qq = Some w} \<le> card {qq. \<mu>q qq = Some v}} = {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mostOftenRcvd \<mu>q = {v}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma common_x_induct:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "SHOcommPerRd Ate_M (HOs (r+k)) (SHOs (r+k))"
  and ih: "card {qq. x (rho (r + k) qq) = v} > E - \<alpha>"
  shows "card {qq. x (rho (r + Suc k) qq) = v} > E - \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
from ih
[PROOF STATE]
proof (chain)
picking this:
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}
[PROOF STEP]
have thrE:"\<forall>pp. card {qq. sendMsg Ate_M (r + k) qq pp (rho (r + k) qq) = v}
                      > E - \<alpha>"
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}

goal (1 subgoal):
 1. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq pp (rho (r + k) qq) = v}
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq pp (rho (r + k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq pp (rho (r + k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
fix qq
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
assume kv:"x (rho (r + k) qq) = v"
[PROOF STATE]
proof (state)
this:
x (rho (r + k) qq) = v

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>qq
      where nxt: "nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq ((rho (Suc (r + k))) qq)"
        and muq: "\<mu>qq \<in> SHOmsgVectors Ate_M (r + k) qq (rho (r + k))
                                         (HOs (r + k) qq) (SHOs (r + k) qq)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<And>\<mu>qq. \<lbrakk>nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq (rho (Suc (r + k)) qq); \<mu>qq \<in> SHOmsgVectors Ate_M (r + k) qq (rho (r + k)) (HOs (r + k) qq) (SHOs (r + k) qq)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq (rho (Suc (r + k)) qq)
\<mu>qq \<in> SHOmsgVectors Ate_M (r + k) qq (rho (r + k)) (HOs (r + k) qq) (SHOs (r + k) qq)

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
have "x (rho (r + Suc k) qq) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x (rho (r + Suc k) qq) = v
[PROOF STEP]
proof (cases "card {pp. \<mu>qq pp \<noteq> None} > T")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
 2. \<not> T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
T < card {pp. \<mu>qq pp \<noteq> None}

goal (2 subgoals):
 1. T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
 2. \<not> T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
[PROOF STEP]
with comm nxt muq thrE
[PROOF STATE]
proof (chain)
picking this:
SHOcommPerRd Ate_M (HOs (r + k)) (SHOs (r + k))
nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq (rho (Suc (r + k)) qq)
\<mu>qq \<in> SHOmsgVectors Ate_M (r + k) qq (rho (r + k)) (HOs (r + k) qq) (SHOs (r + k) qq)
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq pp (rho (r + k) qq) = v}
T < card {pp. \<mu>qq pp \<noteq> None}
[PROOF STEP]
have "mostOftenRcvd \<mu>qq = {v}"
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs (r + k)) (SHOs (r + k))
nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq (rho (Suc (r + k)) qq)
\<mu>qq \<in> SHOmsgVectors Ate_M (r + k) qq (rho (r + k)) (HOs (r + k) qq) (SHOs (r + k) qq)
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq pp (rho (r + k) qq) = v}
T < card {pp. \<mu>qq pp \<noteq> None}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>qq = {v}
[PROOF STEP]
by (auto dest: mostOftenRcvd_v)
[PROOF STATE]
proof (state)
this:
mostOftenRcvd \<mu>qq = {v}

goal (2 subgoals):
 1. T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
 2. \<not> T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
[PROOF STEP]
with nxt True
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq (rho (Suc (r + k)) qq)
T < card {pp. \<mu>qq pp \<noteq> None}
mostOftenRcvd \<mu>qq = {v}
[PROOF STEP]
show "x (rho (r + Suc k) qq) = v"
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq (rho (Suc (r + k)) qq)
T < card {pp. \<mu>qq pp \<noteq> None}
mostOftenRcvd \<mu>qq = {v}

goal (1 subgoal):
 1. x (rho (r + Suc k) qq) = v
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
[PROOF STATE]
proof (state)
this:
x (rho (r + Suc k) qq) = v

goal (1 subgoal):
 1. \<not> T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> T < card {pp. \<mu>qq pp \<noteq> None}

goal (1 subgoal):
 1. \<not> T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
[PROOF STEP]
with nxt
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq (rho (Suc (r + k)) qq)
\<not> T < card {pp. \<mu>qq pp \<noteq> None}
[PROOF STEP]
have "x (rho (r + Suc k) qq) = x (rho (r + k) qq)"
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M (r + k) qq (rho (r + k) qq) \<mu>qq (rho (Suc (r + k)) qq)
\<not> T < card {pp. \<mu>qq pp \<noteq> None}

goal (1 subgoal):
 1. x (rho (r + Suc k) qq) = x (rho (r + k) qq)
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
[PROOF STATE]
proof (state)
this:
x (rho (r + Suc k) qq) = x (rho (r + k) qq)

goal (1 subgoal):
 1. \<not> T < card {pp. \<mu>qq pp \<noteq> None} \<Longrightarrow> x (rho (r + Suc k) qq) = v
[PROOF STEP]
with kv
[PROOF STATE]
proof (chain)
picking this:
x (rho (r + k) qq) = v
x (rho (r + Suc k) qq) = x (rho (r + k) qq)
[PROOF STEP]
show "x (rho (r + Suc k) qq) = v"
[PROOF STATE]
proof (prove)
using this:
x (rho (r + k) qq) = v
x (rho (r + Suc k) qq) = x (rho (r + k) qq)

goal (1 subgoal):
 1. x (rho (r + Suc k) qq) = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x (rho (r + Suc k) qq) = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x (rho (r + Suc k) qq) = v

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x (rho (r + k) ?qq7) = v \<Longrightarrow> x (rho (r + Suc k) ?qq7) = v

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
hence "{qq. x (rho (r + k) qq) = v} \<subseteq> {qq. x (rho (r + Suc k) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
x (rho (r + k) ?qq7) = v \<Longrightarrow> x (rho (r + Suc k) ?qq7) = v

goal (1 subgoal):
 1. {qq. x (rho (r + k) qq) = v} \<subseteq> {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{qq. x (rho (r + k) qq) = v} \<subseteq> {qq. x (rho (r + Suc k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
hence "card {qq. x (rho (r + k) qq) = v} \<le> card {qq. x (rho (r + Suc k) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
{qq. x (rho (r + k) qq) = v} \<subseteq> {qq. x (rho (r + Suc k) qq) = v}

goal (1 subgoal):
 1. card {qq. x (rho (r + k) qq) = v} \<le> card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
by (auto simp: card_mono)
[PROOF STATE]
proof (state)
this:
card {qq. x (rho (r + k) qq) = v} \<le> card {qq. x (rho (r + Suc k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
with ih
[PROOF STATE]
proof (chain)
picking this:
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}
card {qq. x (rho (r + k) qq) = v} \<le> card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}
card {qq. x (rho (r + k) qq) = v} \<le> card {qq. x (rho (r + Suc k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma common_x:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "\<forall>r. SHOcommPerRd (Ate_M::(Proc, 'val::linorder pstate, 'val) SHOMachine)
                              (HOs r) (SHOs r)"
  and d1: "decide (rho r p) \<noteq> Some v"
  and d2: "decide (rho (Suc r) p) = Some v"
  and qupdatex: "x (rho (r + Suc k) q) \<noteq> x (rho (r + k) q)"
  shows "x (rho (r + Suc k) q) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
from comm
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
[PROOF STEP]
have "SHOcommPerRd (Ate_M::(Proc, 'val::linorder pstate, 'val) SHOMachine)
                     (HOs (r+k)) (SHOs (r+k))"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)

goal (1 subgoal):
 1. SHOcommPerRd Ate_M (HOs (r + k)) (SHOs (r + k))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
SHOcommPerRd Ate_M (HOs (r + k)) (SHOs (r + k))

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SHOcommPerRd Ate_M (HOs (r + k)) (SHOs (r + k))

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>q
    where nxt: "nextState Ate_M (r+k) q (rho (r+k) q) \<mu>q (rho (r + Suc k) q)"
      and muq: "\<mu>q \<in> SHOmsgVectors Ate_M (r+k) q (rho (r+k))
                                   (HOs (r+k) q) (SHOs (r+k) q)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<And>\<mu>q. \<lbrakk>nextState Ate_M (r + k) q (rho (r + k) q) \<mu>q (rho (r + Suc k) q); \<mu>q \<in> SHOmsgVectors Ate_M (r + k) q (rho (r + k)) (HOs (r + k) q) (SHOs (r + k) q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
nextState Ate_M (r + k) q (rho (r + k) q) \<mu>q (rho (r + Suc k) q)
\<mu>q \<in> SHOmsgVectors Ate_M (r + k) q (rho (r + k)) (HOs (r + k) q) (SHOs (r + k) q)

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nextState Ate_M (r + k) q (rho (r + k) q) \<mu>q (rho (r + Suc k) q)
\<mu>q \<in> SHOmsgVectors Ate_M (r + k) q (rho (r + k)) (HOs (r + k) q) (SHOs (r + k) q)

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
from nxt qupdatex
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M (r + k) q (rho (r + k) q) \<mu>q (rho (r + Suc k) q)
x (rho (r + Suc k) q) \<noteq> x (rho (r + k) q)
[PROOF STEP]
have threshold_T: "card {qq. \<mu>q qq \<noteq> None} > T"
    and xsmall: "x (rho (r + Suc k) q) = Min (mostOftenRcvd \<mu>q)"
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M (r + k) q (rho (r + k) q) \<mu>q (rho (r + Suc k) q)
x (rho (r + Suc k) q) \<noteq> x (rho (r + k) q)

goal (1 subgoal):
 1. T < card {qq. \<mu>q qq \<noteq> None} &&& x (rho (r + Suc k) q) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
[PROOF STATE]
proof (state)
this:
T < card {qq. \<mu>q qq \<noteq> None}
x (rho (r + Suc k) q) = Min (mostOftenRcvd \<mu>q)

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T < card {qq. \<mu>q qq \<noteq> None}
x (rho (r + Suc k) q) = Min (mostOftenRcvd \<mu>q)

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
have "E - \<alpha> < card {qq. x (rho (r + k) qq) = v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + k) qq) = v}
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. E - \<alpha> < card {qq. x (rho (r + 0) qq) = v}
 2. \<And>k. E - \<alpha> < card {qq. x (rho (r + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
from run comm d1 d2
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v
[PROOF STEP]
have "E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
[PROOF STEP]
by (auto dest: decide_sent_msgs_threshold)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}

goal (2 subgoals):
 1. E - \<alpha> < card {qq. x (rho (r + 0) qq) = v}
 2. \<And>k. E - \<alpha> < card {qq. x (rho (r + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
thus "E - \<alpha> < card {qq. x (rho (r + 0) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + 0) qq) = v}
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. x (rho (r + 0) qq) = v}

goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. x (rho (r + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. x (rho (r + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. x (rho (r + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
assume "E - \<alpha> < card {qq. x (rho (r + k) qq) = v}"
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}

goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. x (rho (r + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
with run comm
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}
[PROOF STEP]
show "E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}
[PROOF STEP]
by (auto dest: common_x_induct)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. x (rho (r + Suc k) qq) = v}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
with run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}
[PROOF STEP]
have "E - \<alpha> < card {qq. sendMsg Ate_M (r+k) qq q (rho (r+k) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
E - \<alpha> < card {qq. x (rho (r + k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = v}
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = v}

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SHOcommPerRd Ate_M (HOs (r + k)) (SHOs (r + k))
nextState Ate_M (r + k) q (rho (r + k) q) \<mu>q (rho (r + Suc k) q)
\<mu>q \<in> SHOmsgVectors Ate_M (r + k) q (rho (r + k)) (HOs (r + k) q) (SHOs (r + k) q)
T < card {qq. \<mu>q qq \<noteq> None}
x (rho (r + Suc k) q) = Min (mostOftenRcvd \<mu>q)
E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = v}
[PROOF STEP]
have "mostOftenRcvd \<mu>q = {v}"
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs (r + k)) (SHOs (r + k))
nextState Ate_M (r + k) q (rho (r + k) q) \<mu>q (rho (r + Suc k) q)
\<mu>q \<in> SHOmsgVectors Ate_M (r + k) q (rho (r + k)) (HOs (r + k) q) (SHOs (r + k) q)
T < card {qq. \<mu>q qq \<noteq> None}
x (rho (r + Suc k) q) = Min (mostOftenRcvd \<mu>q)
E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = v}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
by (auto dest:mostOftenRcvd_v)
[PROOF STATE]
proof (state)
this:
mostOftenRcvd \<mu>q = {v}

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
with xsmall
[PROOF STATE]
proof (chain)
picking this:
x (rho (r + Suc k) q) = Min (mostOftenRcvd \<mu>q)
mostOftenRcvd \<mu>q = {v}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x (rho (r + Suc k) q) = Min (mostOftenRcvd \<mu>q)
mostOftenRcvd \<mu>q = {v}

goal (1 subgoal):
 1. x (rho (r + Suc k) q) = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x (rho (r + Suc k) q) = v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decisionNonNullThenDecided:
  assumes run: "SHORun Ate_M rho HOs SHOs"
      and dec: "decide (rho n p) = Some v"
  obtains m where "m < n"
              and "decide (rho m p) \<noteq> Some v"
              and "decide (rho (Suc m) p) = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m < n; decide (rho m p) \<noteq> Some v; decide (rho (Suc m) p) = Some v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m < n; decide (rho m p) \<noteq> Some v; decide (rho (Suc m) p) = Some v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let "?dec k" = "decide (rho k p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m < n; decide (rho m p) \<noteq> Some v; decide (rho (Suc m) p) = Some v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(\<forall>m<n. ?dec (Suc m) \<noteq> ?dec m \<longrightarrow> ?dec (Suc m) \<noteq> Some v) \<longrightarrow> ?dec n \<noteq> Some v"
    (is "?P n" is "?A n \<longrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<forall>m<0. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho 0 p) \<noteq> Some v
 2. \<And>n. (\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v \<Longrightarrow> (\<forall>m<Suc n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho (Suc n) p) \<noteq> Some v
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
show "?P 0"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<forall>m<0. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho 0 p) \<noteq> Some v
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def SHORun_eq HOinitConfig_eq
                     initState_def Ate_initState_def)
[PROOF STATE]
proof (state)
this:
(\<forall>m<0. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho 0 p) \<noteq> Some v

goal (1 subgoal):
 1. \<And>n. (\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v \<Longrightarrow> (\<forall>m<Suc n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho (Suc n) p) \<noteq> Some v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v \<Longrightarrow> (\<forall>m<Suc n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho (Suc n) p) \<noteq> Some v
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v \<Longrightarrow> (\<forall>m<Suc n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho (Suc n) p) \<noteq> Some v
[PROOF STEP]
assume ih: "?P n"
[PROOF STATE]
proof (state)
this:
(\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v

goal (1 subgoal):
 1. \<And>n. (\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v \<Longrightarrow> (\<forall>m<Suc n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho (Suc n) p) \<noteq> Some v
[PROOF STEP]
thus "?P (Suc n)"
[PROOF STATE]
proof (prove)
using this:
(\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v

goal (1 subgoal):
 1. (\<forall>m<Suc n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho (Suc n) p) \<noteq> Some v
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<forall>m<Suc n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho (Suc n) p) \<noteq> Some v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m < n; decide (rho m p) \<noteq> Some v; decide (rho (Suc m) p) = Some v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with dec that
[PROOF STATE]
proof (chain)
picking this:
decide (rho n p) = Some v
\<lbrakk>?m5 < n; decide (rho ?m5 p) \<noteq> Some v; decide (rho (Suc ?m5) p) = Some v\<rbrakk> \<Longrightarrow> thesis
(\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
decide (rho n p) = Some v
\<lbrakk>?m5 < n; decide (rho ?m5 p) \<noteq> Some v; decide (rho (Suc ?m5) p) = Some v\<rbrakk> \<Longrightarrow> thesis
(\<forall>m<n. decide (rho (Suc m) p) \<noteq> decide (rho m p) \<longrightarrow> decide (rho (Suc m) p) \<noteq> Some v) \<longrightarrow> decide (rho n p) \<noteq> Some v

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed