theory CSpace_AI

lemma (in mdb_insert_abs) untyped_mdb_simple:
  assumes u: "untyped_mdb m cs"
  assumes inc: "untyped_inc m cs"
  assumes src: "cs src = Some c"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes ut: "\<not>is_untyped_cap cap"
  assumes cr: "(obj_refs cap \<subseteq> obj_refs c) \<or>
               (descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c) \<or> safe_parent_for_arch cap c"
  shows "untyped_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" unfolding untyped_mdb_def using u ut cr src dst apply (intro allI impI) apply (simp add: descendants_child) apply (case_tac "ptr = dest", simp) apply simp apply (case_tac "ptr' = dest") apply simp apply (rule impI) apply (elim conjE) apply (simp add: descendants_of_def del: split_paired_All) apply (erule disjE) apply (drule_tac ptr=ptr and ptr'=src in untyped_mdbD, assumption+) apply blast apply assumption apply (simp add: descendants_of_def) apply (erule disjE) apply (elim conjE) apply (case_tac "untyped_range c = {}", simp) apply (frule_tac p=src and p'=ptr in untyped_incD [rotated -1, OF inc]) apply fastforce apply assumption+ apply (simp add: descendants_of_def del: split_paired_All) apply (elim conjE) apply (erule disjE, fastforce) apply (erule disjE, fastforce) apply blast apply (clarsimp dest!: int_not_emptyD safe_parent_for_arch_no_obj_refs) apply (simp add: untyped_mdbD del: split_paired_All) apply (intro impI) apply (frule_tac ptr=src and ptr'=ptr' in untyped_mdbD) apply clarsimp apply assumption apply clarsimp apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<forall>ptr ptr' capa cap'. (cs(dest \<mapsto> cap)) ptr = Some capa \<longrightarrow> is_untyped_cap capa \<longrightarrow> (cs(dest \<mapsto> cap)) ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr (m(dest \<mapsto> src)) proof (prove)
using this:
untyped_mdb m cs
\<not> is_untyped_cap cap
obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c
cs src = Some c
cs dest = Some NullCap

goal (1 subgoal):
 1. \<forall>ptr ptr' capa cap'. (cs(dest \<mapsto> cap)) ptr = Some capa \<longrightarrow> is_untyped_cap capa \<longrightarrow> (cs(dest \<mapsto> cap)) ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; (cs(dest \<mapsto> cap)) ptr = Some capa; is_untyped_cap capa; (cs(dest \<mapsto> cap)) ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; (if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; (if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m)
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; obj_refs cap' \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; obj_refs cap' \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; src \<notin> descendants_of ptr m \<and> ptr \<noteq> src\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; obj_refs cap' \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; src \<notin> descendants_of ptr m; ptr \<noteq> src\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; obj_refs cap' \<subseteq> obj_refs c \<or> (\<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+) \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; obj_refs cap' \<subseteq> obj_refs c\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; (\<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+) \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (5 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; obj_refs cap' \<subseteq> obj_refs c\<rbrakk> \<Longrightarrow> obj_refs c \<inter> untyped_range capa \<noteq> {}
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; obj_refs cap' \<subseteq> obj_refs c\<rbrakk> \<Longrightarrow> untyped_mdb (?m25 ptr ptr' capa cap') cs
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; obj_refs cap' \<subseteq> obj_refs c; src \<in> descendants_of ptr (?m25 ptr ptr' capa cap')\<rbrakk> \<Longrightarrow> False
 4. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; (\<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+) \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 5. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (4 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; obj_refs cap' \<subseteq> obj_refs c\<rbrakk> \<Longrightarrow> untyped_mdb (?m25 ptr ptr' capa cap') cs
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; obj_refs cap' \<subseteq> obj_refs c; src \<in> descendants_of ptr (?m25 ptr ptr' capa cap')\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; (\<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+) \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 4. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; obj_refs cap' \<subseteq> obj_refs c; src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; (\<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+) \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; (\<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+) \<and> obj_refs cap' \<subseteq> untyped_range c \<or> safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; (\<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+) \<and> obj_refs cap' \<subseteq> untyped_range c\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (6 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}\<rbrakk> \<Longrightarrow> is_untyped_cap c
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}\<rbrakk> \<Longrightarrow> cs ptr = Some (?c'104 ptr ptr' capa cap')
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}\<rbrakk> \<Longrightarrow> is_untyped_cap (?c'104 ptr ptr' capa cap')
 4. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}; (untyped_range c \<subseteq> untyped_range (?c'104 ptr ptr' capa cap') \<or> untyped_range (?c'104 ptr ptr' capa cap') \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range (?c'104 ptr ptr' capa cap') = {}) \<and> (untyped_range c \<subset> untyped_range (?c'104 ptr ptr' capa cap') \<longrightarrow> src \<in> descendants_of ptr m \<and> untyped_range c \<inter> usable_untyped_range (?c'104 ptr ptr' capa cap') = {}) \<and> (untyped_range (?c'104 ptr ptr' capa cap') \<subset> untyped_range c \<longrightarrow> ptr \<in> descendants_of src m \<and> untyped_range (?c'104 ptr ptr' capa cap') \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range (?c'104 ptr ptr' capa cap') \<longrightarrow> ptr \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of ptr m \<and> usable_untyped_range (?c'104 ptr ptr' capa cap') = {} \<or> src = ptr)\<rbrakk> \<Longrightarrow> False
 5. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 6. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (5 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}\<rbrakk> \<Longrightarrow> cs ptr = Some (?c'104 ptr ptr' capa cap')
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}\<rbrakk> \<Longrightarrow> is_untyped_cap (?c'104 ptr ptr' capa cap')
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}; (untyped_range c \<subseteq> untyped_range (?c'104 ptr ptr' capa cap') \<or> untyped_range (?c'104 ptr ptr' capa cap') \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range (?c'104 ptr ptr' capa cap') = {}) \<and> (untyped_range c \<subset> untyped_range (?c'104 ptr ptr' capa cap') \<longrightarrow> src \<in> descendants_of ptr m \<and> untyped_range c \<inter> usable_untyped_range (?c'104 ptr ptr' capa cap') = {}) \<and> (untyped_range (?c'104 ptr ptr' capa cap') \<subset> untyped_range c \<longrightarrow> ptr \<in> descendants_of src m \<and> untyped_range (?c'104 ptr ptr' capa cap') \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range (?c'104 ptr ptr' capa cap') \<longrightarrow> ptr \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of ptr m \<and> usable_untyped_range (?c'104 ptr ptr' capa cap') = {} \<or> src = ptr)\<rbrakk> \<Longrightarrow> False
 4. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 5. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}; (untyped_range c \<subseteq> untyped_range capa \<or> untyped_range capa \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range capa = {}) \<and> (untyped_range c \<subset> untyped_range capa \<longrightarrow> src \<in> descendants_of ptr m \<and> untyped_range c \<inter> usable_untyped_range capa = {}) \<and> (untyped_range capa \<subset> untyped_range c \<longrightarrow> ptr \<in> descendants_of src m \<and> untyped_range capa \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range capa \<longrightarrow> ptr \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of ptr m \<and> usable_untyped_range capa = {} \<or> src = ptr)\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}; (untyped_range c \<subseteq> untyped_range capa \<or> untyped_range capa \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range capa = {}) \<and> \<not> untyped_range c \<subset> untyped_range capa \<and> \<not> untyped_range capa \<subset> untyped_range c \<and> untyped_range c \<noteq> untyped_range capa\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}; untyped_range c \<subseteq> untyped_range capa \<or> untyped_range capa \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range capa = {}; \<not> untyped_range c \<subset> untyped_range capa; \<not> untyped_range capa \<subset> untyped_range c; untyped_range c \<noteq> untyped_range capa\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}; \<not> untyped_range c \<subset> untyped_range capa; \<not> untyped_range capa \<subset> untyped_range c; untyped_range c \<noteq> untyped_range capa; untyped_range capa \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; \<forall>x. (src, x) \<notin> (cdt_parent_rel m)\<^sup>+; obj_refs cap' \<subseteq> untyped_range c; untyped_range c \<noteq> {}; \<not> untyped_range c \<subset> untyped_range capa; \<not> untyped_range capa \<subset> untyped_range c; untyped_range c \<noteq> untyped_range capa; untyped_range c \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap'; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cap = cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' = dest; (ptr, src) \<notin> (cdt_parent_rel m)\<^sup>+; ptr \<noteq> src; safe_parent_for_arch cap' c\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; (if ptr' = dest then Some cap else cs ptr') = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m) \<and> (ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m) proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> ptr = src \<longrightarrow> ptr' \<in> descendants_of src m proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m proof (prove)
goal (5 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> is_untyped_cap c
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> cs ptr' = Some (?cap'304 ptr ptr' capa cap')
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> obj_refs (?cap'304 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {}
 4. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> untyped_mdb (?m304 ptr ptr' capa cap') cs
 5. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src; ptr' \<in> descendants_of src (?m304 ptr ptr' capa cap')\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m proof (prove)
goal (4 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> cs ptr' = Some (?cap'304 ptr ptr' capa cap')
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> obj_refs (?cap'304 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {}
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> untyped_mdb (?m304 ptr ptr' capa cap') cs
 4. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src; ptr' \<in> descendants_of src (?m304 ptr ptr' capa cap')\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range c \<noteq> {}
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> untyped_mdb (?m304 ptr ptr' capa cap') cs
 3. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src; ptr' \<in> descendants_of src (?m304 ptr ptr' capa cap')\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src\<rbrakk> \<Longrightarrow> untyped_mdb (?m304 ptr ptr' capa cap') cs
 2. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src; ptr' \<in> descendants_of src (?m304 ptr ptr' capa cap')\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>untyped_mdb m cs; \<not> is_untyped_cap cap; obj_refs cap \<subseteq> obj_refs c \<or> descendants_of src m = {} \<and> obj_refs cap \<subseteq> untyped_range c \<or> safe_parent_for_arch cap c; cs src = Some c; cs dest = Some NullCap; cs ptr = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; ptr \<noteq> dest; ptr' \<noteq> dest; ptr = src; ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m proof (prove)
goal:
No subgoals!