[STATEMENT]
lemma ahm_invar_auxE:
  assumes "ahm_invar_aux bhc n a"
  obtains "\<forall>h. h < array_length a \<longrightarrow> 
      bucket_ok bhc (array_length a) h (array_get a h) \<and> 
      list_map_invar (array_get a h)" and
  "n = array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a" and 
  "array_length a > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<forall>h<array_length a. bucket_ok bhc (array_length a) h (array_get a h) \<and> list_map_invar (array_get a h); n = array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a; 1 < array_length a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ahm_invar_aux bhc n a

goal (1 subgoal):
 1. (\<lbrakk>\<forall>h<array_length a. bucket_ok bhc (array_length a) h (array_get a h) \<and> list_map_invar (array_get a h); n = array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a; 1 < array_length a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ahm_invar_aux_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>h<array_length a. bucket_ok bhc (array_length a) h (array_get a h) \<and> list_map_invar (array_get a h)) \<and> array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a = n \<and> 1 < array_length a

goal (1 subgoal):
 1. (\<lbrakk>\<forall>h<array_length a. bucket_ok bhc (array_length a) h (array_get a h) \<and> list_map_invar (array_get a h); n = array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a; 1 < array_length a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast