diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy
index 4de73f1..a5153d5 100644
--- a/Core_DOM/Core_DOM_Heap_WF.thy
+++ b/Core_DOM/Core_DOM_Heap_WF.thy
@@ -3575,6 +3575,15 @@ assume 1: "xa \<in> fset (object_ptr_kinds h')"
     using heap_is_wellformed_def by blast
 qed
 
+lemma remove_heap_is_wellformed_preserved:
+  assumes "heap_is_wellformed h"
+    and "h \<turnstile> remove child \<rightarrow>\<^sub>h h'"
+    and "known_ptrs h"
+    and type_wf: "type_wf h"
+  shows "type_wf h'" and "known_ptrs h'" and "heap_is_wellformed h'"
+  using assms
+  by(auto simp add: remove_def intro: remove_child_heap_is_wellformed_preserved elim!: bind_returns_heap_E2 split: option.splits)
+
 lemma remove_child_removes_child:
   assumes wellformed: "heap_is_wellformed h"
     and remove_child: "h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h'"
@@ -3728,6 +3737,15 @@ locale l_remove_child_wf2 = l_type_wf + l_known_ptrs + l_remove_child_defs + l_h
   assumes remove_child_heap_is_wellformed_preserved:
     "type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> heap_is_wellformed h \<Longrightarrow> h \<turnstile> remove_child ptr child \<rightarrow>\<^sub>h h'
                \<Longrightarrow> heap_is_wellformed h'"
+  assumes remove_preserves_type_wf: 
+    "heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> remove child \<rightarrow>\<^sub>h h' 
+                          \<Longrightarrow> type_wf h'"
+  assumes remove_preserves_known_ptrs: 
+    "heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> remove child \<rightarrow>\<^sub>h h' 
+                          \<Longrightarrow> known_ptrs h'"
+  assumes remove_heap_is_wellformed_preserved:
+    "type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> heap_is_wellformed h \<Longrightarrow> h \<turnstile> remove child \<rightarrow>\<^sub>h h'
+               \<Longrightarrow> heap_is_wellformed h'"
   assumes remove_child_removes_child:
     "heap_is_wellformed h \<Longrightarrow> h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h' \<Longrightarrow> h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
                           \<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h
@@ -3756,6 +3774,7 @@ lemma remove_child_wf2_is_l_remove_child_wf2 [instances]:
   "l_remove_child_wf2 type_wf known_ptr known_ptrs remove_child heap_is_wellformed get_child_nodes remove"
   apply(auto simp add: l_remove_child_wf2_def l_remove_child_wf2_axioms_def instances)[1]
   using remove_child_heap_is_wellformed_preserved apply(fast, fast, fast)
+  using remove_heap_is_wellformed_preserved apply(fast, fast, fast)
   using remove_child_removes_child apply fast
   using remove_child_removes_first_child apply fast
   using remove_removes_child apply fast
@@ -5161,12 +5180,23 @@ lemma insert_before_wf2_is_l_insert_before_wf2 [instances]:
 
 locale l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
   l_adopt_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
-  l_insert_before_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M  +
-  l_insert_before_wf2  +
+  l_insert_before\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
   l_append_child\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
+  l_insert_before_wf +
+  l_insert_before_wf2  +
   l_get_child_nodes
 begin
 
+
+lemma append_child_heap_is_wellformed_preserved:
+  assumes wellformed: "heap_is_wellformed h"
+    and append_child: "h \<turnstile> append_child ptr node \<rightarrow>\<^sub>h h'"
+    and known_ptrs: "known_ptrs h"
+    and type_wf: "type_wf h"
+  shows "heap_is_wellformed h'" and "type_wf h'" and "known_ptrs h'"
+  using assms
+  by(auto simp add: append_child_def intro: insert_before_preserves_type_wf insert_before_preserves_known_ptrs insert_before_heap_is_wellformed_preserved)
+
 lemma append_child_children:
   assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
   assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r xs"
@@ -5289,6 +5319,17 @@ lemma append_child_for_all_on_no_children:
   by force
 end
 
+locale l_append_child_wf = l_type_wf + l_known_ptrs + l_append_child_defs + l_heap_is_wellformed_defs +
+  assumes append_child_preserves_type_wf: 
+    "heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> append_child ptr child \<rightarrow>\<^sub>h h' 
+                          \<Longrightarrow> type_wf h'"
+  assumes append_child_preserves_known_ptrs: 
+    "heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> append_child ptr child \<rightarrow>\<^sub>h h' 
+                          \<Longrightarrow> known_ptrs h'"
+  assumes append_child_heap_is_wellformed_preserved:
+    "type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> heap_is_wellformed h \<Longrightarrow> h \<turnstile> append_child ptr child \<rightarrow>\<^sub>h h'
+               \<Longrightarrow> heap_is_wellformed h'"
+
 interpretation i_append_child_wf?: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_owner_document get_parent 
                                    get_parent_locs remove_child remove_child_locs 
                                    get_disconnected_nodes get_disconnected_nodes_locs 
@@ -5300,6 +5341,9 @@ interpretation i_append_child_wf?: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^s
                                    parent_child_rel
   by(auto simp add: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
 
+lemma append_child_wf_is_l_append_child_wf [instances]: "l_append_child_wf type_wf known_ptr known_ptrs append_child heap_is_wellformed"
+  apply(auto simp add: l_append_child_wf_def l_append_child_wf_axioms_def instances)
+  using append_child_heap_is_wellformed_preserved by fast+
 
 
 subsection \<open>create\_element\<close>