[STATEMENT]
lemma is_aligned_add_conv:
  fixes off::"'a::len word"
  assumes aligned: "is_aligned w n"
  and        offv: "off < 2 ^ n"
  shows    "to_bl (w + off) =
   (take (LENGTH('a) - n) (to_bl w)) @ (drop (LENGTH('a) - n) (to_bl off))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
 2. \<not> ?P \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
[PROOF STEP]
assume nv: "n \<le> LENGTH('a)"
[PROOF STATE]
proof (state)
this:
n \<le> LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
 2. \<not> ?P \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
[PROOF STEP]
proof (subst aligned_bl_add_size, simp_all only: word_size)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. n \<le> LENGTH('a)
 2. drop (LENGTH('a) - n) (to_bl w) = replicate n False
 3. take (LENGTH('a) - n) (to_bl off) = replicate (LENGTH('a) - n) False
[PROOF STEP]
show "drop (LENGTH('a) - n) (to_bl w) = replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
by (subst is_aligned_replicate [OF aligned nv]) (simp add: word_size)
[PROOF STATE]
proof (state)
this:
drop (LENGTH('a) - n) (to_bl w) = replicate n False

goal (2 subgoals):
 1. n \<le> LENGTH('a)
 2. take (LENGTH('a) - n) (to_bl off) = replicate (LENGTH('a) - n) False
[PROOF STEP]
from offv
[PROOF STATE]
proof (chain)
picking this:
off < 2 ^ n
[PROOF STEP]
show "take (LENGTH('a) - n) (to_bl off) =
                    replicate (LENGTH('a) - n) False"
[PROOF STATE]
proof (prove)
using this:
off < 2 ^ n

goal (1 subgoal):
 1. take (LENGTH('a) - n) (to_bl off) = replicate (LENGTH('a) - n) False
[PROOF STEP]
by (subst less_is_drop_replicate, assumption) simp
[PROOF STATE]
proof (state)
this:
take (LENGTH('a) - n) (to_bl off) = replicate (LENGTH('a) - n) False

goal (1 subgoal):
 1. n \<le> LENGTH('a)
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)

goal (1 subgoal):
 1. \<not> n \<le> LENGTH('a) \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n \<le> LENGTH('a) \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
[PROOF STEP]
assume "\<not> n \<le> LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> n \<le> LENGTH('a)

goal (1 subgoal):
 1. \<not> n \<le> LENGTH('a) \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
[PROOF STEP]
with offv
[PROOF STATE]
proof (chain)
picking this:
off < 2 ^ n
\<not> n \<le> LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
off < 2 ^ n
\<not> n \<le> LENGTH('a)

goal (1 subgoal):
 1. to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
[PROOF STEP]
by (simp add: power_overflow)
[PROOF STATE]
proof (state)
this:
to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_replicateI:
  "to_bl p = addr @ replicate n False \<Longrightarrow> is_aligned (p::'a::len word) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl p = addr @ replicate n False \<Longrightarrow> is_aligned p n
[PROOF STEP]
apply (simp add: is_aligned_to_bl word_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl p = addr @ replicate n False \<Longrightarrow> True \<notin> set (drop (LENGTH('a) - n) addr)
[PROOF STEP]
apply (subgoal_tac "length addr = LENGTH('a) - n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>to_bl p = addr @ replicate n False; length addr = LENGTH('a) - n\<rbrakk> \<Longrightarrow> True \<notin> set (drop (LENGTH('a) - n) addr)
 2. to_bl p = addr @ replicate n False \<Longrightarrow> length addr = LENGTH('a) - n
[PROOF STEP]
apply (simp add: replicate_not_True)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl p = addr @ replicate n False \<Longrightarrow> length addr = LENGTH('a) - n
[PROOF STEP]
apply (drule arg_cong [where f=length])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (to_bl p) = length (addr @ replicate n False) \<Longrightarrow> length addr = LENGTH('a) - n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma to_bl_2p:
  "n < LENGTH('a) \<Longrightarrow>
   to_bl ((2::'a::len word) ^ n) =
   replicate (LENGTH('a) - Suc n) False @ True # replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> to_bl (2 ^ n) = replicate (LENGTH('a) - Suc n) False @ True # replicate n False
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n < LENGTH('a) \<Longrightarrow> length (to_bl (2 ^ n)) = length (replicate (LENGTH('a) - Suc n) False @ True # replicate n False)
 2. \<And>i. \<lbrakk>n < LENGTH('a); i < length (to_bl (2 ^ n))\<rbrakk> \<Longrightarrow> to_bl (2 ^ n) ! i = (replicate (LENGTH('a) - Suc n) False @ True # replicate n False) ! i
[PROOF STEP]
apply (auto simp add: nth_append to_bl_nth word_size bit_simps not_less nth_Cons le_diff_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>n < LENGTH('a); i < LENGTH('a); LENGTH('a) \<le> Suc (i + n); case Suc (i + n) - LENGTH('a) of 0 \<Rightarrow> True | Suc k \<Rightarrow> replicate n False ! k\<rbrakk> \<Longrightarrow> n = LENGTH('a) - Suc i
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); i < LENGTH('a); LENGTH('a) \<le> Suc (i + n); case Suc (i + n) - LENGTH('a) of 0 \<Rightarrow> True | Suc k \<Rightarrow> replicate n False ! k\<rbrakk> \<Longrightarrow> n = LENGTH('a) - Suc i
[PROOF STEP]
apply (cases \<open>Suc (i + n) - LENGTH('a)\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); i < LENGTH('a); LENGTH('a) \<le> Suc (i + n); case Suc (i + n) - LENGTH('a) of 0 \<Rightarrow> True | Suc k \<Rightarrow> replicate n False ! k; Suc (i + n) - LENGTH('a) = 0\<rbrakk> \<Longrightarrow> n = LENGTH('a) - Suc i
 2. \<And>nat. \<lbrakk>n < LENGTH('a); i < LENGTH('a); LENGTH('a) \<le> Suc (i + n); case Suc (i + n) - LENGTH('a) of 0 \<Rightarrow> True | Suc k \<Rightarrow> replicate n False ! k; Suc (i + n) - LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> n = LENGTH('a) - Suc i
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma xor_2p_to_bl:
  fixes x::"'a::len word"
  shows "to_bl (x XOR 2^n) =
  (if n < LENGTH('a)
   then take (LENGTH('a)-Suc n) (to_bl x) @ (\<not>rev (to_bl x)!n) # drop (LENGTH('a)-n) (to_bl x)
   else to_bl x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (x XOR 2 ^ n) = (if n < LENGTH('a) then take (LENGTH('a) - Suc n) (to_bl x) @ (\<not> rev (to_bl x) ! n) # drop (LENGTH('a) - n) (to_bl x) else to_bl x)
[PROOF STEP]
apply (auto simp add: to_bl_eq_rev take_map drop_map take_rev drop_rev bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> map (bit (x XOR 2 ^ n)) (rev [0..<LENGTH('a)]) = map (bit x) (rev [Suc n..<LENGTH('a)]) @ (\<not> rev (map (bit x) (rev [0..<LENGTH('a)])) ! n) # map (bit x) (rev [0..<n])
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n < LENGTH('a) \<Longrightarrow> length (map (bit (x XOR 2 ^ n)) (rev [0..<LENGTH('a)])) = length (map (bit x) (rev [Suc n..<LENGTH('a)]) @ (\<not> rev (map (bit x) (rev [0..<LENGTH('a)])) ! n) # map (bit x) (rev [0..<n]))
 2. \<And>i. \<lbrakk>n < LENGTH('a); i < length (map (bit (x XOR 2 ^ n)) (rev [0..<LENGTH('a)]))\<rbrakk> \<Longrightarrow> map (bit (x XOR 2 ^ n)) (rev [0..<LENGTH('a)]) ! i = (map (bit x) (rev [Suc n..<LENGTH('a)]) @ (\<not> rev (map (bit x) (rev [0..<LENGTH('a)])) ! n) # map (bit x) (rev [0..<n])) ! i
[PROOF STEP]
apply (auto simp add: bit_simps rev_nth nth_append Suc_diff_Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_replicateD:
  "\<lbrakk> is_aligned (w::'a::len word) n; n \<le> LENGTH('a) \<rbrakk>
     \<Longrightarrow> \<exists>xs. to_bl w = xs @ replicate n False
               \<and> length xs = size w - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> \<exists>xs. to_bl w = xs @ replicate n False \<and> length xs = size w - n
[PROOF STEP]
apply (subst is_aligned_replicate, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> \<exists>xs. take (LENGTH('a) - n) (to_bl w) @ replicate n False = xs @ replicate n False \<and> length xs = size w - n
[PROOF STEP]
apply (rule exI, rule conjI, rule refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> length (take (LENGTH('a) - n) (to_bl w)) = size w - n
[PROOF STEP]
apply (simp add: word_size)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_pad_to_length:
  assumes lbl: "length bl \<le> sz"
  shows   "length (bl_pad_to bl sz) = sz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bl_pad_to bl sz) = sz
[PROOF STEP]
using lbl
[PROOF STATE]
proof (prove)
using this:
length bl \<le> sz

goal (1 subgoal):
 1. length (bl_pad_to bl sz) = sz
[PROOF STEP]
by (simp add: bl_pad_to_def)


[STATEMENT]
lemma bl_pad_to_prefix:
  "prefix bl (bl_pad_to bl sz)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix bl (bl_pad_to bl sz)
[PROOF STEP]
by (simp add: bl_pad_to_def)


[STATEMENT]
lemma of_bl_length:
  "length xs < LENGTH('a) \<Longrightarrow> of_bl xs < (2 :: 'a::len word) ^ length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs < LENGTH('a) \<Longrightarrow> of_bl xs < 2 ^ length xs
[PROOF STEP]
by (simp add: of_bl_length_less)


[STATEMENT]
lemma of_bl_mult_and_not_mask_eq:
  "\<lbrakk>is_aligned (a :: 'a::len word) n; length b + m \<le> n\<rbrakk>
   \<Longrightarrow> a + of_bl b * (2^m) AND NOT(mask n) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ m AND NOT (mask n) = a
[PROOF STEP]
apply (simp flip: push_bit_eq_mult subtract_mask(1) take_bit_eq_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n (a + push_bit m (of_bl b))
[PROOF STEP]
apply (subst disjunctive_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> \<not> bit a na \<or> \<not> bit (push_bit m (of_bl b)) na
 2. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n (a OR push_bit m (of_bl b))
[PROOF STEP]
apply (auto simp add: bit_simps not_le not_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned a n; length b + m \<le> n; rev b ! (na - m); bit a na; m \<le> na; na < LENGTH('a); na - m < length b\<rbrakk> \<Longrightarrow> LENGTH('a) \<le> na - m
 2. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n a OR take_bit n (push_bit m (of_bl b))
[PROOF STEP]
apply (meson is_aligned_imp_not_bit is_aligned_weaken less_diff_conv2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n a OR take_bit n (push_bit m (of_bl b))
[PROOF STEP]
apply (erule is_alignedE')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>length b + m \<le> n; a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n a OR take_bit n (push_bit m (of_bl b))
[PROOF STEP]
apply (simp add: take_bit_push_bit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>length b + m \<le> n; a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = push_bit m (take_bit (n - m) (of_bl b))
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q na. \<lbrakk>length b + m \<le> n; a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (push_bit m (of_bl b)) na = bit (push_bit m (take_bit (n - m) (of_bl b))) na
[PROOF STEP]
apply (auto simp add: bit_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_to_bl_of_bl_eq:
  "\<lbrakk>is_aligned (a::'a::len word) n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk>
  \<Longrightarrow> bin_to_bl (length b) (uint ((a + of_bl b * 2^c) >> c)) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a + of_bl b * 2 ^ c >> c)) = b
[PROOF STEP]
apply (simp flip: push_bit_eq_mult take_bit_eq_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length b) (uint (a + push_bit c (of_bl b) >> c)) [] = b
[PROOF STEP]
apply (subst disjunctive_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> bit a na \<or> \<not> bit (push_bit c (of_bl b)) na
 2. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length b) (uint (a OR push_bit c (of_bl b) >> c)) [] = b
[PROOF STEP]
apply (auto simp add: bit_simps not_le not_less unsigned_or_eq unsigned_drop_bit_eq
     unsigned_push_bit_eq bin_to_bl_or simp flip: bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a); rev b ! (na - c); bit a na; c \<le> na; na < LENGTH('a); na - c < length b\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)) = b
[PROOF STEP]
apply (meson is_aligned_imp_not_bit is_aligned_weaken less_diff_conv2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)) = b
[PROOF STEP]
apply (erule is_alignedE')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)) = b
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> length (bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c))) = length b
 2. \<And>q i. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n); i < length (bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)))\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)) ! i = b ! i
[PROOF STEP]
apply (auto simp add: nth_bin_to_bl bit_simps rev_nth simp flip: bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_cast_long_short_long_ingoreLeadingZero_generic:
  "\<lbrakk> length (dropWhile Not (to_bl w)) \<le> LENGTH('s); LENGTH('s) \<le> LENGTH('l) \<rbrakk> \<Longrightarrow>
   (of_bl :: _ \<Rightarrow> 'l::len word) (to_bl ((of_bl::_ \<Rightarrow> 's::len word) (to_bl w))) = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (dropWhile Not (to_bl w)) \<le> LENGTH('s); LENGTH('s) \<le> LENGTH('l)\<rbrakk> \<Longrightarrow> of_bl (to_bl (of_bl (to_bl w))) = w
[PROOF STEP]
by (rule word_uint_eqI) (simp add: uint_of_bl_is_bl_to_bin uint_of_bl_is_bl_to_bin_drop)


[STATEMENT]
lemma length_drop_mask:
  fixes w::"'a::len word"
  shows "length (dropWhile Not (to_bl (w AND mask n))) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (dropWhile Not (to_bl (w AND mask n))) \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (dropWhile Not (to_bl (w AND mask n))) \<le> n
[PROOF STEP]
have "length (takeWhile Not (replicate n False @ ls)) = n + length (takeWhile Not ls)"
    for ls n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (replicate n False @ ls)) = n + length (takeWhile Not ls)
[PROOF STEP]
by(subst takeWhile_append2) simp+
[PROOF STATE]
proof (state)
this:
length (takeWhile Not (replicate ?n False @ ?ls)) = ?n + length (takeWhile Not ?ls)

goal (1 subgoal):
 1. length (dropWhile Not (to_bl (w AND mask n))) \<le> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (takeWhile Not (replicate ?n False @ ?ls)) = ?n + length (takeWhile Not ?ls)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (takeWhile Not (replicate ?n False @ ?ls)) = ?n + length (takeWhile Not ?ls)

goal (1 subgoal):
 1. length (dropWhile Not (to_bl (w AND mask n))) \<le> n
[PROOF STEP]
unfolding bl_and_mask
[PROOF STATE]
proof (prove)
using this:
length (takeWhile Not (replicate ?n False @ ?ls)) = ?n + length (takeWhile Not ?ls)

goal (1 subgoal):
 1. length (dropWhile Not (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w))) \<le> n
[PROOF STEP]
by (simp add: dropWhile_eq_drop)
[PROOF STATE]
proof (state)
this:
length (dropWhile Not (to_bl (w AND mask n))) \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_bits_rev_to_bl:
  "map (bit x) [0..<size x] = rev (to_bl x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (bit x) [0..<size x] = rev (to_bl x)
[PROOF STEP]
by (auto simp: list_eq_iff_nth_eq test_bit_bl word_size)


[STATEMENT]
lemma of_bl_length2:
  "length xs + c < LENGTH('a) \<Longrightarrow> of_bl xs * 2^c < (2::'a::len word) ^ (length xs + c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs + c < LENGTH('a) \<Longrightarrow> of_bl xs * 2 ^ c < 2 ^ (length xs + c)
[PROOF STEP]
by (simp add: of_bl_length word_less_power_trans2)


[STATEMENT]
lemma of_bl_max:
  "(of_bl xs :: 'a::len word) \<le> mask (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs)
[PROOF STEP]
define ys where \<open>ys = rev xs\<close>
[PROOF STATE]
proof (state)
this:
ys = rev xs

goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs)
[PROOF STEP]
have \<open>take_bit (length ys) (horner_sum of_bool 2 ys :: 'a word) = horner_sum of_bool 2 ys\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit (length ys) (horner_sum of_bool 2 ys) = horner_sum of_bool 2 ys
[PROOF STEP]
by transfer (simp add: take_bit_horner_sum_bit_eq min_def)
[PROOF STATE]
proof (state)
this:
take_bit (length ys) (horner_sum of_bool 2 ys) = horner_sum of_bool 2 ys

goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take_bit (length ys) (horner_sum of_bool 2 ys) = horner_sum of_bool 2 ys
[PROOF STEP]
have \<open>(of_bl (rev ys) :: 'a word) \<le> mask (length ys)\<close>
[PROOF STATE]
proof (prove)
using this:
take_bit (length ys) (horner_sum of_bool 2 ys) = horner_sum of_bool 2 ys

goal (1 subgoal):
 1. of_bl (rev ys) \<le> mask (length ys)
[PROOF STEP]
by (simp only: of_bl_rev_eq less_eq_mask_iff_take_bit_eq_self)
[PROOF STATE]
proof (state)
this:
of_bl (rev ys) \<le> mask (length ys)

goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs)
[PROOF STEP]
with ys_def
[PROOF STATE]
proof (chain)
picking this:
ys = rev xs
of_bl (rev ys) \<le> mask (length ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = rev xs
of_bl (rev ys) \<le> mask (length ys)

goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_bl xs \<le> mask (length xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sshiftr_clamp_pos:
  assumes
    "LENGTH('a) \<le> n"
    "0 \<le> sint x"
  shows "(x::'a::len word) >>> n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x >>> n = 0
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit 0 na
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
LENGTH('a) \<le> n
0 \<le> sint x

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit 0 na
[PROOF STEP]
apply (auto simp add: bit_simps bit_last_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sshiftr_clamp_neg:
  assumes
    "LENGTH('a) \<le> n"
    "sint x < 0"
  shows "(x::'a::len word) >>> n = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x >>> n = - 1
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit (- 1) na
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
LENGTH('a) \<le> n
sint x < 0

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit (- 1) na
[PROOF STEP]
apply (auto simp add: bit_simps bit_last_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sshiftr_clamp:
  assumes "LENGTH('a) \<le> n"
  shows "(x::'a::len word) >>> n = x >>> LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x >>> n = x >>> LENGTH('a)
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit (x >>> LENGTH('a)) na
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
LENGTH('a) \<le> n

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit (x >>> LENGTH('a)) na
[PROOF STEP]
apply (auto simp add: bit_simps bit_last_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sshiftr1_bl_of:
  "length bl = LENGTH('a) \<Longrightarrow>
    sshiftr1 (of_bl bl::'a::len word) = of_bl (hd bl # butlast bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl = LENGTH('a) \<Longrightarrow> sshiftr1 (of_bl bl) = of_bl (hd bl # butlast bl)
[PROOF STEP]
apply (rule word_bl.Rep_eqD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl = LENGTH('a) \<Longrightarrow> to_bl (sshiftr1 (of_bl bl)) = to_bl (of_bl (hd bl # butlast bl))
[PROOF STEP]
apply (subst bl_sshiftr1[of "of_bl bl :: 'a word"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl = LENGTH('a) \<Longrightarrow> hd (to_bl (of_bl bl)) # butlast (to_bl (of_bl bl)) = to_bl (of_bl (hd bl # butlast bl))
[PROOF STEP]
by (simp add: word_bl.Abs_inverse)


[STATEMENT]
lemma sshiftr1_bl_of':
  "LENGTH('a) \<le> length bl \<Longrightarrow>
    sshiftr1 (of_bl bl::'a::len word) =
    of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> length bl \<Longrightarrow> sshiftr1 (of_bl bl) = of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))
[PROOF STEP]
apply (subst of_bl_drop'[symmetric, of "length bl - LENGTH('a)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. LENGTH('a) \<le> length bl \<Longrightarrow> length bl - LENGTH('a) = length bl - LENGTH('a)
 2. LENGTH('a) \<le> length bl \<Longrightarrow> sshiftr1 (of_bl (drop (length bl - LENGTH('a)) bl)) = of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))
[PROOF STEP]
using sshiftr1_bl_of[of "drop (length bl - LENGTH('a)) bl"]
[PROOF STATE]
proof (prove)
using this:
length (drop (length bl - LENGTH('a)) bl) = LENGTH(?'a) \<Longrightarrow> sshiftr1 (of_bl (drop (length bl - LENGTH('a)) bl)) = of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))

goal (2 subgoals):
 1. LENGTH('a) \<le> length bl \<Longrightarrow> length bl - LENGTH('a) = length bl - LENGTH('a)
 2. LENGTH('a) \<le> length bl \<Longrightarrow> sshiftr1 (of_bl (drop (length bl - LENGTH('a)) bl)) = of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))
[PROOF STEP]
by auto


[STATEMENT]
lemma sshiftr_bl_of:
  assumes "length bl = LENGTH('a)"
  shows "(of_bl bl::'a::len word) >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
length bl = LENGTH('a)
[PROOF STEP]
obtain b bs where \<open>bl = b # bs\<close>
[PROOF STATE]
proof (prove)
using this:
length bl = LENGTH('a)

goal (1 subgoal):
 1. (\<And>b bs. bl = b # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases bl) simp_all
[PROOF STATE]
proof (state)
this:
bl = b # bs

goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bl = b # bs
[PROOF STEP]
have *: \<open>bl ! 0 \<longleftrightarrow> b\<close> \<open>hd bl \<longleftrightarrow> b\<close>
[PROOF STATE]
proof (prove)
using this:
bl = b # bs

goal (1 subgoal):
 1. bl ! 0 = b &&& hd bl = b
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
bl ! 0 = b
hd bl = b

goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (of_bl bl >>> n) na = bit (of_bl (replicate n (hd bl) @ take (length bl - n) bl)) na
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
length bl = LENGTH('a)
bl ! 0 = b
hd bl = b

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (of_bl bl >>> n) na = bit (of_bl (replicate n (hd bl) @ take (length bl - n) bl)) na
[PROOF STEP]
by (auto simp add: bit_simps nth_append rev_nth not_less)
[PROOF STATE]
proof (state)
this:
of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sshiftr_bl: "x >>> n \<equiv> of_bl (replicate n (msb x) @ take (LENGTH('a) - n) (to_bl x))"
  for x :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x >>> n \<equiv> of_bl (replicate n (msb x) @ take (LENGTH('a) - n) (to_bl x))
[PROOF STEP]
unfolding word_msb_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x >>> n \<equiv> of_bl (replicate n (hd (to_bl x)) @ take (LENGTH('a) - n) (to_bl x))
[PROOF STEP]
by (smt (z3) length_to_bl_eq sshiftr_bl_of word_bl.Rep_inverse)


[STATEMENT]
lemma of_bl_drop_eq_take_bit:
  \<open>of_bl (drop n xs) = take_bit (length xs - n) (of_bl xs)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (drop n xs) = take_bit (length xs - n) (of_bl xs)
[PROOF STEP]
by (simp add: of_bl_drop take_bit_eq_mask)


[STATEMENT]
lemma of_bl_take_to_bl_eq_drop_bit:
  \<open>of_bl (take n (to_bl w)) = drop_bit (LENGTH('a) - n) w\<close>
    if \<open>n \<le> LENGTH('a)\<close>
    for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (take n (to_bl w)) = drop_bit (LENGTH('a) - n) w
[PROOF STEP]
using that shiftr_bl [of w \<open>LENGTH('a) - n\<close>]
[PROOF STATE]
proof (prove)
using this:
n \<le> LENGTH('a)
w >> LENGTH('a) - n \<equiv> of_bl (take (LENGTH('a) - (LENGTH('a) - n)) (to_bl w))

goal (1 subgoal):
 1. of_bl (take n (to_bl w)) = drop_bit (LENGTH('a) - n) w
[PROOF STEP]
by (simp add: shiftr_def)


[STATEMENT]
lemma link_size[simp]: "size (link hp) = size hp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (link hp) = size hp
[PROOF STEP]
by (cases hp rule: link.cases) simp_all


[STATEMENT]
lemma size_pass\<^sub>1: "size (pass\<^sub>1 hp) = size hp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (pass\<^sub>1 hp) = size hp
[PROOF STEP]
by (induct hp rule: pass\<^sub>1.induct) simp_all


[STATEMENT]
lemma size_pass\<^sub>2: "size (pass\<^sub>2 hp) = size hp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (pass\<^sub>2 hp) = size hp
[PROOF STEP]
by (induct hp rule: pass\<^sub>2.induct) simp_all


[STATEMENT]
lemma size_merge:
  "is_root h1 \<Longrightarrow> is_root h2 \<Longrightarrow> size (merge h1 h2) = size h1 + size h2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_root h1; is_root h2\<rbrakk> \<Longrightarrow> size (merge h1 h2) = size h1 + size h2
[PROOF STEP]
by (simp split: tree.splits)


[STATEMENT]
lemma \<Delta>\<Phi>_insert: "is_root hp \<Longrightarrow> \<Phi> (insert x hp) - \<Phi> hp \<le> log 2  (size hp + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_root hp \<Longrightarrow> \<Phi> (Pairing_Heap_Tree.insert x hp) - \<Phi> hp \<le> log 2 (real (size hp + 1))
[PROOF STEP]
by (simp split: tree.splits)


[STATEMENT]
lemma \<Delta>\<Phi>_merge:
  assumes "h1 = Node hs1 x1 Leaf" "h2 = Node hs2 x2 Leaf"
  shows "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (size h1 + size h2) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
let ?hs = "Node hs1 x1 (Node hs2 x2 Leaf)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
have "\<Phi> (merge h1 h2) = \<Phi> (link ?hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (merge h1 h2) = \<Phi> (link \<langle>hs1, x1, \<langle>hs2, x2, \<langle>\<rangle>\<rangle>\<rangle>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h1 = \<langle>hs1, x1, \<langle>\<rangle>\<rangle>
h2 = \<langle>hs2, x2, \<langle>\<rangle>\<rangle>

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) = \<Phi> (link \<langle>hs1, x1, \<langle>hs2, x2, \<langle>\<rangle>\<rangle>\<rangle>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Phi> (merge h1 h2) = \<Phi> (link \<langle>hs1, x1, \<langle>hs2, x2, \<langle>\<rangle>\<rangle>\<rangle>)

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (merge h1 h2) = \<Phi> (link \<langle>hs1, x1, \<langle>hs2, x2, \<langle>\<rangle>\<rangle>\<rangle>)

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
have "\<dots> = \<Phi> hs1 + \<Phi> hs2 + log 2 (size hs1 + size hs2 + 1) + log 2 (size hs1 + size hs2 + 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (link \<langle>hs1, x1, \<langle>hs2, x2, \<langle>\<rangle>\<rangle>\<rangle>) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size hs1 + size hs2 + 2))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
\<Phi> (link \<langle>hs1, x1, \<langle>hs2, x2, \<langle>\<rangle>\<rangle>\<rangle>) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size hs1 + size hs2 + 2))

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (link \<langle>hs1, x1, \<langle>hs2, x2, \<langle>\<rangle>\<rangle>\<rangle>) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size hs1 + size hs2 + 2))

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
have "\<dots> = \<Phi> hs1 + \<Phi> hs2 + log 2 (size hs1 + size hs2 + 1) + log 2 (size h1 + size h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size hs1 + size hs2 + 2)) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h1 = \<langle>hs1, x1, \<langle>\<rangle>\<rangle>
h2 = \<langle>hs2, x2, \<langle>\<rangle>\<rangle>

goal (1 subgoal):
 1. \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size hs1 + size hs2 + 2)) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size hs1 + size hs2 + 2)) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2))

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Phi> (merge h1 h2) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2))
[PROOF STEP]
have "\<Phi> (merge h1 h2) = \<dots>"
[PROOF STATE]
proof (prove)
using this:
\<Phi> (merge h1 h2) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2))

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Phi> (merge h1 h2) = \<Phi> hs1 + \<Phi> hs2 + log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2))

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
have "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 =
   log 2 (size hs1 + size hs2 + 1) + log 2 (size h1 + size h2)
   - log 2 (size hs1 + 1) - log 2 (size hs2 + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 = log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2)) - log 2 (real (size hs1 + 1)) - log 2 (real (size hs2 + 1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h1 = \<langle>hs1, x1, \<langle>\<rangle>\<rangle>
h2 = \<langle>hs2, x2, \<langle>\<rangle>\<rangle>

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 = log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2)) - log 2 (real (size hs1 + 1)) - log 2 (real (size hs2 + 1))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 = log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2)) - log 2 (real (size hs1 + 1)) - log 2 (real (size hs2 + 1))

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 = log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2)) - log 2 (real (size hs1 + 1)) - log 2 (real (size hs2 + 1))

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
have "\<dots> \<le> log 2 (size h1 + size h2) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2)) - log 2 (real (size hs1 + 1)) - log 2 (real (size hs2 + 1)) \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
using ld_le_2ld[of "size hs1" "size hs2"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> real (size hs1); 0 \<le> real (size hs2)\<rbrakk> \<Longrightarrow> log 2 (1 + real (size hs1) + real (size hs2)) \<le> 1 + log 2 (1 + real (size hs1)) + log 2 (1 + real (size hs2))
h1 = \<langle>hs1, x1, \<langle>\<rangle>\<rangle>
h2 = \<langle>hs2, x2, \<langle>\<rangle>\<rangle>

goal (1 subgoal):
 1. log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2)) - log 2 (real (size hs1 + 1)) - log 2 (real (size hs2 + 1)) \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size h1 + size h2)) - log 2 (real (size hs1 + 1)) - log 2 (real (size hs2 + 1)) \<le> log 2 (real (size h1 + size h2)) + 1

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1

goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<Delta>\<Phi>_pass1: "\<Phi> (pass\<^sub>1 hs) - \<Phi> hs  \<le> 2 * log 2 (size hs + 1) - len hs + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
proof (induction hs rule: pass\<^sub>1.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
case (1 hs1 x hs2 y hs)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
let ?h = "Node hs1 x (Node hs2 y hs)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
let ?n1 = "size hs1"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
let ?n2 = "size hs2"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
let ?m = "size hs"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
have "\<Phi> (pass\<^sub>1 ?h) - \<Phi> ?h = \<Phi> (pass\<^sub>1 hs) + log 2 (?n1+?n2+1) - \<Phi> hs - log 2 (?n2+?m+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>1 \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> = \<Phi> (pass\<^sub>1 hs) + log 2 (real (size hs1 + size hs2 + 1)) - \<Phi> hs - log 2 (real (size hs2 + size hs + 1))
[PROOF STEP]
by (simp add: size_pass\<^sub>1 algebra_simps)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>1 \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> = \<Phi> (pass\<^sub>1 hs) + log 2 (real (size hs1 + size hs2 + 1)) - \<Phi> hs - log 2 (real (size hs2 + size hs + 1))

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>1 \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> = \<Phi> (pass\<^sub>1 hs) + log 2 (real (size hs1 + size hs2 + 1)) - \<Phi> hs - log 2 (real (size hs2 + size hs + 1))

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
have "\<dots> \<le> log 2 (?n1+?n2+1) - log 2 (?n2+?m+1) + 2 * log 2 (?m + 1) - len hs + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>1 hs) + log 2 (real (size hs1 + size hs2 + 1)) - \<Phi> hs - log 2 (real (size hs2 + size hs + 1)) \<le> log 2 (real (size hs1 + size hs2 + 1)) - log 2 (real (size hs2 + size hs + 1)) + 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
using "1.IH"
[PROOF STATE]
proof (prove)
using this:
\<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>1 hs) + log 2 (real (size hs1 + size hs2 + 1)) - \<Phi> hs - log 2 (real (size hs2 + size hs + 1)) \<le> log 2 (real (size hs1 + size hs2 + 1)) - log 2 (real (size hs2 + size hs + 1)) + 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>1 hs) + log 2 (real (size hs1 + size hs2 + 1)) - \<Phi> hs - log 2 (real (size hs2 + size hs + 1)) \<le> log 2 (real (size hs1 + size hs2 + 1)) - log 2 (real (size hs2 + size hs + 1)) + 2 * log 2 (real (size hs + 1)) - real (len hs) + 2

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>1 hs) + log 2 (real (size hs1 + size hs2 + 1)) - \<Phi> hs - log 2 (real (size hs2 + size hs + 1)) \<le> log 2 (real (size hs1 + size hs2 + 1)) - log 2 (real (size hs2 + size hs + 1)) + 2 * log 2 (real (size hs + 1)) - real (len hs) + 2

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
have "\<dots> \<le> 2 * log 2 (?n1+?n2+?m+2) - log 2 (?n2+?m+1) + log 2 (?m + 1) - len hs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (real (size hs1 + size hs2 + 1)) - log 2 (real (size hs2 + size hs + 1)) + 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<le> 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - log 2 (real (size hs2 + size hs + 1)) + log 2 (real (size hs + 1)) - real (len hs)
[PROOF STEP]
using ld_sum_inequality [of "?n1+?n2+1" "?m + 1"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < real (size hs1 + size hs2 + 1); 0 < real (size hs + 1)\<rbrakk> \<Longrightarrow> log 2 (real (size hs1 + size hs2 + 1)) + log 2 (real (size hs + 1)) + 2 \<le> 2 * log 2 (real (size hs1 + size hs2 + 1) + real (size hs + 1))

goal (1 subgoal):
 1. log 2 (real (size hs1 + size hs2 + 1)) - log 2 (real (size hs2 + size hs + 1)) + 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<le> 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - log 2 (real (size hs2 + size hs + 1)) + log 2 (real (size hs + 1)) - real (len hs)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
log 2 (real (size hs1 + size hs2 + 1)) - log 2 (real (size hs2 + size hs + 1)) + 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<le> 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - log 2 (real (size hs2 + size hs + 1)) + log 2 (real (size hs + 1)) - real (len hs)

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
log 2 (real (size hs1 + size hs2 + 1)) - log 2 (real (size hs2 + size hs + 1)) + 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<le> 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - log 2 (real (size hs2 + size hs + 1)) + log 2 (real (size hs + 1)) - real (len hs)

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
have "\<dots> \<le> 2 * log 2 (?n1+?n2+?m+2) - len hs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - log 2 (real (size hs2 + size hs + 1)) + log 2 (real (size hs + 1)) - real (len hs) \<le> 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - real (len hs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - log 2 (real (size hs2 + size hs + 1)) + log 2 (real (size hs + 1)) - real (len hs) \<le> 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - real (len hs)

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - log 2 (real (size hs2 + size hs + 1)) + log 2 (real (size hs + 1)) - real (len hs) \<le> 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - real (len hs)

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
have "\<dots> = 2 * log 2 (size ?h) - len ?h + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - real (len hs) = 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - real (len hs) = 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * log 2 (real (size hs1 + size hs2 + size hs + 2)) - real (len hs) = 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
have "\<dots> \<le> 2 * log 2 (size ?h + 1) - len ?h + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2 \<le> 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2 \<le> 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2

goal (3 subgoals):
 1. \<And>hsx x hsy y hs. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2 \<Longrightarrow> \<Phi> (pass\<^sub>1 \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hsx, x, \<langle>hsy, y, hs\<rangle>\<rangle>) + 2
 2. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 3. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Phi> (pass\<^sub>1 \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Phi> (pass\<^sub>1 \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>1 \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>1 \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) - \<Phi> \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle> + 1)) - real (len \<langle>hs1, x, \<langle>hs2, y, hs\<rangle>\<rangle>) + 2

goal (2 subgoals):
 1. \<Phi> (pass\<^sub>1 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> 2 * log 2 (real (size \<langle>\<rangle> + 1)) - real (len \<langle>\<rangle>) + 2
 2. \<And>v va. \<Phi> (pass\<^sub>1 \<langle>v, va, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>v, va, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size \<langle>v, va, \<langle>\<rangle>\<rangle> + 1)) - real (len \<langle>v, va, \<langle>\<rangle>\<rangle>) + 2
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma \<Delta>\<Phi>_pass2: "hs \<noteq> Leaf \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (size hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs))
[PROOF STEP]
proof (induction hs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<langle>\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> log 2 (real (size \<langle>\<rangle>))
 2. \<And>hs1 x2 hs2. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs2 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs2) - \<Phi> hs2 \<le> log 2 (real (size hs2)); \<langle>hs1, x2, hs2\<rangle> \<noteq> \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x2, hs2\<rangle>) - \<Phi> \<langle>hs1, x2, hs2\<rangle> \<le> log 2 (real (size \<langle>hs1, x2, hs2\<rangle>))
[PROOF STEP]
case (Node hs1 x hs)
[PROOF STATE]
proof (state)
this:
hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1))
hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs))
\<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>

goal (2 subgoals):
 1. \<langle>\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> log 2 (real (size \<langle>\<rangle>))
 2. \<And>hs1 x2 hs2. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs2 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs2) - \<Phi> hs2 \<le> log 2 (real (size hs2)); \<langle>hs1, x2, hs2\<rangle> \<noteq> \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x2, hs2\<rangle>) - \<Phi> \<langle>hs1, x2, hs2\<rangle> \<le> log 2 (real (size \<langle>hs1, x2, hs2\<rangle>))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1))
hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs))
\<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
proof (cases hs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
case 1: (Node hs2 y r)
[PROOF STATE]
proof (state)
this:
hs = \<langle>hs2, y, r\<rangle>

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
let ?h = "Node hs1 x hs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
obtain hs3 a where 2: "pass\<^sub>2 hs = Node hs3 a Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>hs3 a. pass\<^sub>2 hs = \<langle>hs3, a, \<langle>\<rangle>\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pass\<^sub>2_struct 1
[PROOF STATE]
proof (prove)
using this:
\<exists>l a. pass\<^sub>2 \<langle>?hs1.0, ?x, ?hs\<rangle> = \<langle>l, a, \<langle>\<rangle>\<rangle>
hs = \<langle>hs2, y, r\<rangle>

goal (1 subgoal):
 1. (\<And>hs3 a. pass\<^sub>2 hs = \<langle>hs3, a, \<langle>\<rangle>\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
pass\<^sub>2 hs = \<langle>hs3, a, \<langle>\<rangle>\<rangle>

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
hence 3: "size hs = size \<dots>"
[PROOF STATE]
proof (prove)
using this:
pass\<^sub>2 hs = \<langle>hs3, a, \<langle>\<rangle>\<rangle>

goal (1 subgoal):
 1. size hs = size \<langle>hs3, a, \<langle>\<rangle>\<rangle>
[PROOF STEP]
using size_pass\<^sub>2
[PROOF STATE]
proof (prove)
using this:
pass\<^sub>2 hs = \<langle>hs3, a, \<langle>\<rangle>\<rangle>
size (pass\<^sub>2 ?hp) = size ?hp

goal (1 subgoal):
 1. size hs = size \<langle>hs3, a, \<langle>\<rangle>\<rangle>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
size hs = size \<langle>hs3, a, \<langle>\<rangle>\<rangle>

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
have link: "\<Phi>(link(Node hs1 x (pass\<^sub>2 hs))) - \<Phi> hs1 - \<Phi> (pass\<^sub>2 hs) =
          log 2 (size hs1 + size hs + 1) + log 2 (size hs1 + size hs) - log 2 (size hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> (pass\<^sub>2 hs) = log 2 (real (size hs1 + size hs + 1)) + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs))
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
pass\<^sub>2 hs = \<langle>hs3, a, \<langle>\<rangle>\<rangle>
size hs = size \<langle>hs3, a, \<langle>\<rangle>\<rangle>

goal (1 subgoal):
 1. \<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> (pass\<^sub>2 hs) = log 2 (real (size hs1 + size hs + 1)) + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
\<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> (pass\<^sub>2 hs) = log 2 (real (size hs1 + size hs + 1)) + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs))

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
have "\<Phi> (pass\<^sub>2 ?h) - \<Phi> ?h =
        \<Phi> (link (Node hs1 x (pass\<^sub>2 hs))) - \<Phi> hs1 - \<Phi> hs - log 2 (size hs1 + size hs + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> = \<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> hs - log 2 (real (size hs1 + size hs + 1))
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> = \<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> hs - log 2 (real (size hs1 + size hs + 1))

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> = \<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> hs - log 2 (real (size hs1 + size hs + 1))

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
have "\<dots> = \<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (size hs1 + size hs) - log 2 (size hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> hs - log 2 (real (size hs1 + size hs + 1)) = \<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs))
[PROOF STEP]
using link
[PROOF STATE]
proof (prove)
using this:
\<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> (pass\<^sub>2 hs) = log 2 (real (size hs1 + size hs + 1)) + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs))

goal (1 subgoal):
 1. \<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> hs - log 2 (real (size hs1 + size hs + 1)) = \<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> hs - log 2 (real (size hs1 + size hs + 1)) = \<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs))

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (link \<langle>hs1, x, pass\<^sub>2 hs\<rangle>) - \<Phi> hs1 - \<Phi> hs - log 2 (real (size hs1 + size hs + 1)) = \<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs))

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
have "\<dots> \<le> log 2 (size hs1 + size hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs)) \<le> log 2 (real (size hs1 + size hs))
[PROOF STEP]
using Node.IH(2) 1
[PROOF STATE]
proof (prove)
using this:
hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs))
hs = \<langle>hs2, y, r\<rangle>

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs)) \<le> log 2 (real (size hs1 + size hs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs)) \<le> log 2 (real (size hs1 + size hs))

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 hs) - \<Phi> hs + log 2 (real (size hs1 + size hs)) - log 2 (real (size hs)) \<le> log 2 (real (size hs1 + size hs))

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
have "\<dots> \<le> log 2 (size ?h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (real (size hs1 + size hs)) \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
hs = \<langle>hs2, y, r\<rangle>

goal (1 subgoal):
 1. log 2 (real (size hs1 + size hs)) \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
log 2 (real (size hs1 + size hs)) \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))

goal (2 subgoals):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
 2. \<And>x21 x22 x23. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))

goal (1 subgoal):
 1. \<lbrakk>hs1 \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs1) - \<Phi> hs1 \<le> log 2 (real (size hs1)); hs \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (real (size hs)); \<langle>hs1, x, hs\<rangle> \<noteq> \<langle>\<rangle>; hs = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 \<langle>hs1, x, hs\<rangle>) - \<Phi> \<langle>hs1, x, hs\<rangle> \<le> log 2 (real (size \<langle>hs1, x, hs\<rangle>))

goal (1 subgoal):
 1. \<langle>\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> \<Phi> (pass\<^sub>2 \<langle>\<rangle>) - \<Phi> \<langle>\<rangle> \<le> log 2 (real (size \<langle>\<rangle>))
[PROOF STEP]
qed simp


[STATEMENT]
lemma \<Delta>\<Phi>_del_min:
  "\<Phi> (del_min (Node hs x Leaf)) - \<Phi> (Node hs x Leaf)
  \<le> 2 * log 2 (size hs + 1) - len hs + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
have "\<Phi> (del_min (Node hs x Leaf)) - \<Phi> (Node hs x Leaf) =
        \<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - (log 2 (1 + real (size hs)) + \<Phi> hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> = \<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - (log 2 (1 + real (size hs)) + \<Phi> hs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> = \<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - (log 2 (1 + real (size hs)) + \<Phi> hs)

goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> = \<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - (log 2 (1 + real (size hs)) + \<Phi> hs)

goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
have "\<dots> \<le> \<Phi> (pass\<^sub>1 hs) - \<Phi> hs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - (log 2 (1 + real (size hs)) + \<Phi> hs) \<le> \<Phi> (pass\<^sub>1 hs) - \<Phi> hs
[PROOF STEP]
using \<Delta>\<Phi>_pass2' [of "pass\<^sub>1 hs"]
[PROOF STATE]
proof (prove)
using this:
\<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - \<Phi> (pass\<^sub>1 hs) \<le> log 2 (real (size (pass\<^sub>1 hs) + 1))

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - (log 2 (1 + real (size hs)) + \<Phi> hs) \<le> \<Phi> (pass\<^sub>1 hs) - \<Phi> hs
[PROOF STEP]
by(simp add: size_pass\<^sub>1)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - (log 2 (1 + real (size hs)) + \<Phi> hs) \<le> \<Phi> (pass\<^sub>1 hs) - \<Phi> hs

goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (pass\<^sub>1 hs)) - (log 2 (1 + real (size hs)) + \<Phi> hs) \<le> \<Phi> (pass\<^sub>1 hs) - \<Phi> hs

goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
have "\<dots> \<le> 2 * log 2 (size hs + 1) - len hs + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
by(rule \<Delta>\<Phi>_pass1)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2

goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2

goal (1 subgoal):
 1. \<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min \<langle>hs, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs + 1)) - real (len hs) + 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_root_merge:
  "is_root h1 \<Longrightarrow> is_root h2 \<Longrightarrow> is_root (merge h1 h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_root h1; is_root h2\<rbrakk> \<Longrightarrow> is_root (merge h1 h2)
[PROOF STEP]
by (simp split: tree.splits)


[STATEMENT]
lemma is_root_insert: "is_root h \<Longrightarrow> is_root (insert x h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_root h \<Longrightarrow> is_root (Pairing_Heap_Tree.insert x h)
[PROOF STEP]
by (simp split: tree.splits)


[STATEMENT]
lemma is_root_del_min:
  assumes "is_root h" shows "is_root (del_min h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_root (del_min h)
[PROOF STEP]
proof (cases h)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. h = \<langle>\<rangle> \<Longrightarrow> is_root (del_min h)
 2. \<And>x21 x22 x23. h = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
case [simp]: (Node hs1 x hs)
[PROOF STATE]
proof (state)
this:
h = \<langle>hs1, x, hs\<rangle>

goal (2 subgoals):
 1. h = \<langle>\<rangle> \<Longrightarrow> is_root (del_min h)
 2. \<And>x21 x22 x23. h = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
have "hs = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hs = \<langle>\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_root h

goal (1 subgoal):
 1. hs = \<langle>\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hs = \<langle>\<rangle>

goal (2 subgoals):
 1. h = \<langle>\<rangle> \<Longrightarrow> is_root (del_min h)
 2. \<And>x21 x22 x23. h = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
hs = \<langle>\<rangle>

goal (1 subgoal):
 1. is_root (del_min h)
[PROOF STEP]
proof (cases hs1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
 2. \<And>x21 x22 x23. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
case (Node hs2 y hs')
[PROOF STATE]
proof (state)
this:
hs1 = \<langle>hs2, y, hs'\<rangle>

goal (2 subgoals):
 1. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
 2. \<And>x21 x22 x23. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hs1 = \<langle>hs2, y, hs'\<rangle>
[PROOF STEP]
obtain la a ra where "pass\<^sub>1 hs1 = Node a la ra"
[PROOF STATE]
proof (prove)
using this:
hs1 = \<langle>hs2, y, hs'\<rangle>

goal (1 subgoal):
 1. (\<And>a la ra. pass\<^sub>1 hs1 = \<langle>a, la, ra\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pass\<^sub>1_struct
[PROOF STATE]
proof (prove)
using this:
hs1 = \<langle>hs2, y, hs'\<rangle>
\<exists>l a r. pass\<^sub>1 \<langle>?hs1.0, ?x, ?hs\<rangle> = \<langle>l, a, r\<rangle>

goal (1 subgoal):
 1. (\<And>a la ra. pass\<^sub>1 hs1 = \<langle>a, la, ra\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pass\<^sub>1 hs1 = \<langle>a, la, ra\<rangle>

goal (2 subgoals):
 1. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
 2. \<And>x21 x22 x23. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pass\<^sub>1 hs1 = \<langle>a, la, ra\<rangle>

goal (2 subgoals):
 1. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
 2. \<And>x21 x22 x23. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
obtain lb b where "pass\<^sub>2 \<dots> = Node b lb Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b lb. pass\<^sub>2 \<langle>a, la, ra\<rangle> = \<langle>b, lb, \<langle>\<rangle>\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pass\<^sub>2_struct
[PROOF STATE]
proof (prove)
using this:
\<exists>l a. pass\<^sub>2 \<langle>?hs1.0, ?x, ?hs\<rangle> = \<langle>l, a, \<langle>\<rangle>\<rangle>

goal (1 subgoal):
 1. (\<And>b lb. pass\<^sub>2 \<langle>a, la, ra\<rangle> = \<langle>b, lb, \<langle>\<rangle>\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pass\<^sub>2 \<langle>a, la, ra\<rangle> = \<langle>b, lb, \<langle>\<rangle>\<rangle>

goal (2 subgoals):
 1. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
 2. \<And>x21 x22 x23. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>x21, x22, x23\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pass\<^sub>1 hs1 = \<langle>a, la, ra\<rangle>
pass\<^sub>2 \<langle>a, la, ra\<rangle> = \<langle>b, lb, \<langle>\<rangle>\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pass\<^sub>1 hs1 = \<langle>a, la, ra\<rangle>
pass\<^sub>2 \<langle>a, la, ra\<rangle> = \<langle>b, lb, \<langle>\<rangle>\<rangle>

goal (1 subgoal):
 1. is_root (del_min h)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pass\<^sub>1 hs1 = \<langle>a, la, ra\<rangle>
pass\<^sub>2 \<langle>a, la, ra\<rangle> = \<langle>b, lb, \<langle>\<rangle>\<rangle>
is_root h

goal (1 subgoal):
 1. is_root (del_min h)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_root (del_min h)

goal (1 subgoal):
 1. \<lbrakk>hs = \<langle>\<rangle>; hs1 = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
is_root (del_min h)

goal (1 subgoal):
 1. h = \<langle>\<rangle> \<Longrightarrow> is_root (del_min h)
[PROOF STEP]
qed simp


[STATEMENT]
lemma pass\<^sub>1_len: "len (pass\<^sub>1 h) \<le> len h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. len (pass\<^sub>1 h) \<le> len h
[PROOF STEP]
by (induct h rule: pass\<^sub>1.induct) simp_all