diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy
index 8f10787..eebd0f2 100644
--- a/Core_DOM/Core_DOM_Heap_WF.thy
+++ b/Core_DOM/Core_DOM_Heap_WF.thy
@@ -2494,7 +2494,7 @@ subsection \<open>get\_owner\_document\<close>
 locale l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
   l_known_ptrs
   + l_heap_is_wellformed
-  + l_get_root_node
+  + l_get_root_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
   + l_get_ancestors
   + l_get_ancestors_wf
   + l_get_parent
@@ -2807,11 +2807,93 @@ proof -
      apply (simp add: assms(1) assms(2) assms(3) local.get_root_node_ok)
     using assms(3) local.get_disconnected_nodes_ok by blast
 qed
+
+lemma get_owner_document_child_same:
+  assumes "heap_is_wellformed h"  "known_ptrs h" "type_wf h"
+  assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
+  assumes "child \<in> set children"
+  shows "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> get_owner_document (cast child) \<rightarrow>\<^sub>r owner_document"
+proof -
+  have "ptr |\<in>| object_ptr_kinds h"
+    by (meson assms(4) is_OK_returns_result_I local.get_child_nodes_ptr_in_heap) 
+  then have "known_ptr ptr"
+    using assms(2) local.known_ptrs_known_ptr by blast 
+
+  have "cast child |\<in>| object_ptr_kinds h"
+    using assms(1) assms(4) assms(5) local.heap_is_wellformed_children_in_heap node_ptr_kinds_commutes by blast 
+  then
+  have "known_ptr (cast child)"
+    using assms(2) local.known_ptrs_known_ptr by blast 
+
+  obtain root where root: "h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root"
+    by (meson \<open>ptr |\<in>| object_ptr_kinds h\<close> assms(1) assms(2) assms(3) is_OK_returns_result_E local.get_root_node_ok) 
+  then have "h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root"
+    using assms(1) assms(2) assms(3) assms(4) assms(5) local.child_parent_dual local.get_root_node_parent_same by blast 
+
+  have "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \<rightarrow>\<^sub>r owner_document"
+  proof (cases "is_document_ptr ptr")
+    case True
+    then obtain document_ptr where document_ptr: "cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^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 document_ptr = ptr"
+      using case_optionE document_ptr_casts_commute by blast 
+    then have "root = cast document_ptr"
+      using root
+      by(auto simp add: get_root_node_def get_ancestors_def elim!: bind_returns_result_E2 split: option.splits)
+       
+    then have "h \<turnstile> a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr () \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \<rightarrow>\<^sub>r owner_document"
+      using document_ptr \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr] 
+      apply(auto simp add:  a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 dest!: bind_returns_result_E3[rotated, OF \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr], rotated] intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: if_splits option.splits)
+      using \<open>ptr |\<in>| object_ptr_kinds h\<close> document_ptr_kinds_commutes by blast
+    then show ?thesis
+      using \<open>known_ptr ptr\<close>
+      apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_impl)
+       apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
+          apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
+          apply(drule(1)  known_ptr_not_character_data_ptr)
+          apply(drule(1)  known_ptr_not_element_ptr)
+          apply(simp add: NodeClass.known_ptr_defs)
+      using \<open>ptr |\<in>| object_ptr_kinds h\<close> True
+      by(auto simp add: document_ptr[symmetric] intro!: bind_pure_returns_result_I split: option.splits)
+  next
+    case False
+    then obtain node_ptr where node_ptr: "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^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 node_ptr = ptr"
+      using \<open>known_ptr ptr\<close>
+      by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
+    then have "h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \<rightarrow>\<^sub>r owner_document"
+      using root \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>
+      unfolding a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
+      by (meson bind_pure_returns_result_I bind_returns_result_E3 local.get_root_node_pure)
+    then show ?thesis
+      using \<open>known_ptr ptr\<close>
+      apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_impl)
+       apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
+          apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
+          apply(drule(1)  known_ptr_not_character_data_ptr)
+          apply(drule(1)  known_ptr_not_element_ptr)
+          apply(simp add: NodeClass.known_ptr_defs)
+      using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
+         apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
+      apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
+         apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
+      by (meson invoke_empty is_OK_returns_result_I)
+  qed
+  then show ?thesis
+    using \<open>known_ptr (cast child)\<close>
+    apply(auto simp add: get_owner_document_def[of "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^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 child"] a_get_owner_document_tups_def known_ptr_impl)
+     apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
+        apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
+        apply(drule(1)  known_ptr_not_character_data_ptr)
+        apply(drule(1)  known_ptr_not_element_ptr)
+        apply(simp add: NodeClass.known_ptr_defs)
+    using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
+       apply(auto intro!: bind_pure_returns_result_I split: option.splits)
+    by (smt \<open>cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^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 child |\<in>| object_ptr_kinds h\<close> cast_document_ptr_not_node_ptr(1) comp_apply invoke_empty invoke_not invoke_returns_result is_OK_returns_result_I node_ptr_casts_commute2 option.sel)
+qed
+
 end
 
 locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs 
                                + l_get_disconnected_nodes_defs + l_get_owner_document_defs 
-                               + l_get_parent_defs +
+                               + l_get_parent_defs + l_get_child_nodes_defs +
   assumes get_owner_document_disconnected_nodes:
     "heap_is_wellformed h \<Longrightarrow>
      known_ptrs h \<Longrightarrow>
@@ -2832,26 +2914,24 @@ locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known
  assumes get_owner_document_ok: 
     "heap_is_wellformed h \<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h 
                           \<Longrightarrow> h \<turnstile> ok (get_owner_document ptr)"
+  assumes get_owner_document_child_same:
+    "heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children \<Longrightarrow> child \<in> set children \<Longrightarrow> h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> get_owner_document (cast child) \<rightarrow>\<^sub>r owner_document"
 
-
-interpretation i_get_owner_document_wf?:
-  l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M known_ptr known_ptrs type_wf heap_is_wellformed parent_child_rel 
-  get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs 
-  get_root_node get_root_node_locs get_parent get_parent_locs get_ancestors get_ancestors_locs 
-  get_owner_document
-  by(simp add: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
+interpretation i_get_owner_document_wf?: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
+    known_ptr known_ptrs type_wf heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs get_parent get_parent_locs get_ancestors get_ancestors_locs get_root_node get_root_node_locs get_owner_document
+  by(auto simp add: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
 declare l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
 
-
 lemma get_owner_document_wf_is_l_get_owner_document_wf [instances]:
   "l_get_owner_document_wf heap_is_wellformed type_wf known_ptr known_ptrs get_disconnected_nodes 
-                           get_owner_document get_parent"
+                           get_owner_document get_parent get_child_nodes"
   using known_ptrs_is_l_known_ptrs
   apply(auto simp add: l_get_owner_document_wf_def l_get_owner_document_wf_axioms_def)
   using get_owner_document_disconnected_nodes apply fast
   using  in_disconnected_nodes_no_parent apply fast
   using get_owner_document_owner_document_in_heap apply fast
   using get_owner_document_ok apply fast
+  using get_owner_document_child_same apply (fast, fast)
   done