[STATEMENT]
lemma start_addrs_NewHeapElem_start_heap_obsD:
  "a \<in> set start_addrs \<Longrightarrow> \<exists>CTn. NewHeapElem a CTn \<in> set start_heap_obs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> set start_addrs \<Longrightarrow> \<exists>CTn. NewHeapElem a CTn \<in> set start_heap_obs
[PROOF STEP]
using length_initialization_list_le_length_start_addrs
[PROOF STATE]
proof (prove)
using this:
length start_addrs \<le> length initialization_list

goal (1 subgoal):
 1. a \<in> set start_addrs \<Longrightarrow> \<exists>CTn. NewHeapElem a CTn \<in> set start_heap_obs
[PROOF STEP]
unfolding start_heap_obs_def start_addrs_def
[PROOF STATE]
proof (prove)
using this:
length (fst (snd start_heap_data)) \<le> length initialization_list

goal (1 subgoal):
 1. a \<in> set (fst (snd start_heap_data)) \<Longrightarrow> \<exists>CTn. NewHeapElem a CTn \<in> set (map2 (\<lambda>C a. NewHeapElem a (Class_type C)) initialization_list (fst (snd start_heap_data)))
[PROOF STEP]
by(force simp add: set_zip in_set_conv_nth intro: rev_image_eqI)