diff --git a/Core_DOM/preliminaries/Heap_Error_Monad.thy b/Core_DOM/preliminaries/Heap_Error_Monad.thy
index e035a64..853056d 100644
--- a/Core_DOM/preliminaries/Heap_Error_Monad.thy
+++ b/Core_DOM/preliminaries/Heap_Error_Monad.thy
@@ -79,9 +79,23 @@ definition
   where
     "returns_heap h p h' \<longleftrightarrow> (case h \<turnstile> p of Inr (_ , h'') \<Rightarrow> h' = h'' | Inl _ \<Rightarrow> False)"
 
+fun select_heap ("|(_)|\<^sub>h")
+  where
+    "select_heap (Inr ( _, h)) = h"
+  | "select_heap (Inl _) = undefined"
+
 lemma returns_heap_eq [elim]: "h \<turnstile> f \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h'' \<Longrightarrow> h' = h''"
   by(auto simp add: returns_heap_def split: sum.splits)
 
+definition 
+  returns_result_heap :: "'heap \<Rightarrow> ('heap, 'e, 'result) prog \<Rightarrow> 'result \<Rightarrow> 'heap \<Rightarrow> bool" 
+  ("((_)/ \<turnstile> (_)/ \<rightarrow>\<^sub>r (_) \<rightarrow>\<^sub>h (_))" [60, 35, 61, 62] 65)
+  where
+    "returns_result_heap h p r h' \<longleftrightarrow> h \<turnstile> p \<rightarrow>\<^sub>r r \<and> h \<turnstile> p \<rightarrow>\<^sub>h h'"
+
+lemma [code]: "returns_result_heap h p r h' \<longleftrightarrow> (case h \<turnstile> p of Inr (r', h'') \<Rightarrow> r = r' \<and> h' = h'' | Inl _ \<Rightarrow> False)" 
+  by(auto simp add: returns_result_heap_def returns_result_def returns_heap_def split: sum.splits)
+
 definition 
   returns_error :: "'heap \<Rightarrow> ('heap, 'e, 'result) prog \<Rightarrow> 'e \<Rightarrow> bool" 
   ("((_)/ \<turnstile> (_)/ \<rightarrow>\<^sub>e (_))" [60, 35, 61] 65)