[STATEMENT]
lemma get_root_node_si_root_in_heap:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_root_node_si ptr \<rightarrow>\<^sub>r root"
  shows "root |\<in>| object_ptr_kinds h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root |\<in>| object_ptr_kinds h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
heap_is_wellformed h
type_wf h
known_ptrs h
h \<turnstile> get_root_node_si ptr \<rightarrow>\<^sub>r root

goal (1 subgoal):
 1. root |\<in>| object_ptr_kinds h
[PROOF STEP]
apply(auto simp add: get_root_node_si_def elim!: bind_returns_result_E2)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>heap_is_wellformed h; type_wf h; known_ptrs h; h \<turnstile> get_ancestors_si ptr \<rightarrow>\<^sub>r x; root = last x\<rbrakk> \<Longrightarrow> last x |\<in>| object_ptr_kinds h
[PROOF STEP]
by (simp add: get_ancestors_si_never_empty get_ancestors_si_ptrs_in_heap)