[STATEMENT]
theorem pred_bound_size_univ': "invar_vebt t n \<Longrightarrow> u =  2^n \<Longrightarrow>   T\<^sub>p\<^sub>r\<^sub>e\<^sub>d' t x \<le> 2 + lb (lb u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; u = 2 ^ n\<rbrakk> \<Longrightarrow> real (T\<^sub>p\<^sub>r\<^sub>e\<^sub>d' t x) \<le> 2 + log 2 (log 2 u)
[PROOF STEP]
using pred_bound_height'[of t n x] height_double_log_univ_size[of u n t]
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n \<Longrightarrow> T\<^sub>p\<^sub>r\<^sub>e\<^sub>d' t x \<le> 1 + height t
\<lbrakk>u = 2 ^ n; invar_vebt t n\<rbrakk> \<Longrightarrow> real (height t) \<le> 1 + log 2 (log 2 u)

goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; u = 2 ^ n\<rbrakk> \<Longrightarrow> real (T\<^sub>p\<^sub>r\<^sub>e\<^sub>d' t x) \<le> 2 + log 2 (log 2 u)
[PROOF STEP]
by simp