[STATEMENT]
lemma get_child_nodes_new_element:
  "ptr' \<noteq> cast new_element_ptr \<Longrightarrow> h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr \<Longrightarrow> h \<turnstile> new_element \<rightarrow>\<^sub>h h'
     \<Longrightarrow> r \<in> get_child_nodes_locs ptr' \<Longrightarrow> r h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr' \<noteq> cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr; h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr; h \<turnstile> new_element \<rightarrow>\<^sub>h h'; r \<in> get_child_nodes_locs ptr'\<rbrakk> \<Longrightarrow> r h h'
[PROOF STEP]
by (auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def new_element_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t new_element_get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
      new_element_get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t new_element_get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t split: prod.splits if_splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)