diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy
index d87cc7a..8f10787 100644
--- a/Core_DOM/Core_DOM_Heap_WF.thy
+++ b/Core_DOM/Core_DOM_Heap_WF.thy
@@ -2785,6 +2785,28 @@ next
   qed
 qed
 
+lemma get_owner_document_ok: 
+  assumes "heap_is_wellformed h"  "known_ptrs h" "type_wf h"
+  assumes "ptr |\<in>| object_ptr_kinds h"
+  shows "h \<turnstile> ok (get_owner_document ptr)"
+proof -
+  have "known_ptr ptr"
+    using assms(2) assms(4) local.known_ptrs_known_ptr
+    by blast
+  then show ?thesis
+    apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)
+    apply(split invoke_splits, (rule conjI | rule impI)+)+
+       apply(auto simp add: known_ptr_impl)[1]
+    using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr known_ptr_not_element_ptr apply blast
+    using assms(4)
+      apply(auto simp add: 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 a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)
+        apply (metis (no_types, lifting) document_ptr_casts_commute3 document_ptr_kinds_commutes is_document_ptr_kind_none option.case_eq_if)
+       apply (metis (no_types, lifting) assms(1) assms(2) assms(3) is_node_ptr_kind_none local.get_root_node_ok node_ptr_casts_commute3 option.case_eq_if)
+      apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)
+    using assms(3) local.get_disconnected_nodes_ok apply blast
+     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
 end
 
 locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs 
@@ -2807,6 +2829,9 @@ locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known
     node_ptr \<in> set disc_nodes"
  assumes get_owner_document_owner_document_in_heap: 
     "heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<Longrightarrow> owner_document |\<in>| document_ptr_kinds h"
+ 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)"
 
 
 interpretation i_get_owner_document_wf?:
@@ -2826,6 +2851,7 @@ lemma get_owner_document_wf_is_l_get_owner_document_wf [instances]:
   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
   done
 
 
diff --git a/Core_DOM/monads/ObjectMonad.thy b/Core_DOM/monads/ObjectMonad.thy
index 038bf37..69c3a86 100644
--- a/Core_DOM/monads/ObjectMonad.thy
+++ b/Core_DOM/monads/ObjectMonad.thy
@@ -244,4 +244,15 @@ proof -
     using object_ptr_kinds_preserved_small by blast
 qed
 
+
+lemma reads_writes_preserved2:
+  assumes "writes SW setter h h'"
+  assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
+  assumes "\<And>h h' x. \<forall>w \<in> SW. h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr getter) h h'"
+  shows "preserved (get_M ptr getter) h h'"
+  apply(clarsimp simp add: preserved_def)
+  using reads_singleton assms(1) assms(2)
+  apply(rule reads_writes_preserved)
+  using assms(3)
+  by(auto simp add: preserved_def)
 end