theory CNodeInv_R

lemma descendants_of_subset_untyped:
  assumes adj: "\<And>x. ((m x = None) = (m' x = None))
                   \<and> (\<forall>cte cte'. m x = Some cte \<and> m' x = Some cte'
                       \<longrightarrow> (isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte'))
                         \<and> (capRange (cteCap cte) = capRange (cteCap cte'))
                         \<and> (isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = cteCap cte'))"
  and    desc: "\<And>x. descendants_of' x m \<subseteq> descendants_of' x m'"
  shows        "(untyped_inc' m \<longrightarrow> untyped_inc' m')
                     \<and> (untyped_mdb' m \<longrightarrow> untyped_mdb' m')" proof have P: "\<And>x cte. \<lbrakk> m' x = Some cte; isUntypedCap (cteCap cte) \<rbrakk>
                       \<Longrightarrow> \<exists>node. m x = Some (CTE (cteCap cte) node) \<and> m' x = Some cte" apply (cut_tac x=x in adj) apply clarsimp apply (case_tac y, simp) done show "untyped_inc' m \<longrightarrow> untyped_inc' m'" unfolding untyped_inc'_def apply (rule impI, erule allEI, erule allEI) apply clarsimp apply (drule P | simp)+ apply clarsimp apply (cut_tac x=p in desc) apply (cut_tac x=p' in desc) apply blast done have Q: "\<And>x cte. m' x = Some cte
             \<Longrightarrow> \<exists>cap node. m x = Some (CTE cap node)
                    \<and> isUntypedCap cap = isUntypedCap (cteCap cte)
                    \<and> capRange cap = capRange (cteCap cte)" apply (cut_tac x=x in adj) apply clarsimp apply (case_tac y, simp) done show "untyped_mdb' m \<longrightarrow> untyped_mdb' m'" unfolding untyped_mdb'_def apply (rule impI, erule allEI, erule allEI) apply clarsimp apply (drule_tac x=p in P, simp) apply (drule_tac x=p' in Q, simp) apply clarsimp apply (cut_tac x=p in desc) apply blast done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (untyped_inc' m \<longrightarrow> untyped_inc' m') \<and> (untyped_mdb' m \<longrightarrow> untyped_mdb' m') proof (state)
goal (2 subgoals):
 1. untyped_inc' m \<longrightarrow> untyped_inc' m'
 2. untyped_mdb' m \<longrightarrow> untyped_mdb' m' proof (prove)
goal (1 subgoal):
 1. \<And>x cte. \<lbrakk>m' x = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> \<exists>node. m x = Some (CTE (cteCap cte) node) \<and> m' x = Some cte proof (prove)
goal (1 subgoal):
 1. \<And>x cte. \<lbrakk>m' x = Some cte; isUntypedCap (cteCap cte); (m x = None) = (m' x = None) \<and> (\<forall>cte cte'. m x = Some cte \<and> m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> (isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = cteCap cte'))\<rbrakk> \<Longrightarrow> \<exists>node. m x = Some (CTE (cteCap cte) node) \<and> m' x = Some cte proof (prove)
goal (1 subgoal):
 1. \<And>x cte y. \<lbrakk>m' x = Some cte; isUntypedCap (cteCap cte); m x = Some y; cteCap y = cteCap cte\<rbrakk> \<Longrightarrow> \<exists>node. y = CTE (cteCap cte) node proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m' ?x = Some ?cte; isUntypedCap (cteCap ?cte)\<rbrakk> \<Longrightarrow> \<exists>node. m ?x = Some (CTE (cteCap ?cte) node) \<and> m' ?x = Some ?cte

goal (2 subgoals):
 1. untyped_inc' m \<longrightarrow> untyped_inc' m'
 2. untyped_mdb' m \<longrightarrow> untyped_mdb' m' proof (prove)
goal (1 subgoal):
 1. untyped_inc' m \<longrightarrow> untyped_inc' m' proof (prove)
goal (1 subgoal):
 1. (\<forall>p p' c c' n n'. m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m p' = Some (CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')) \<longrightarrow> (\<forall>p p' c c' n n'. m' p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m' p' = Some (CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<forall>c c' n n'. m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m p' = Some (CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p') \<Longrightarrow> \<forall>c c' n n'. m' p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m' p' = Some (CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')); m' p = Some (CTE c n); isUntypedCap c; m' p' = Some (CTE c' n'); isUntypedCap c'\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')); isUntypedCap c; isUntypedCap c'; (\<exists>node. m p = Some (CTE c node)) \<and> m' p = Some (CTE c n); (\<exists>node. m p' = Some (CTE c' node)) \<and> m' p' = Some (CTE c' n')\<rbrakk> \<Longrightarrow> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m') \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m') \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' node nodea. \<lbrakk>isUntypedCap c; isUntypedCap c'; m' p = Some (CTE c n); m p = Some (CTE c node); m' p' = Some (CTE c' n'); m p' = Some (CTE c' nodea); untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}; untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p'\<rbrakk> \<Longrightarrow> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m') \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m') \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' node nodea. \<lbrakk>isUntypedCap c; isUntypedCap c'; m' p = Some (CTE c n); m p = Some (CTE c node); m' p' = Some (CTE c' n'); m p' = Some (CTE c' nodea); untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}; untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p'; descendants_of' p m \<subseteq> descendants_of' p m'\<rbrakk> \<Longrightarrow> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m') \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m') \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' node nodea. \<lbrakk>isUntypedCap c; isUntypedCap c'; m' p = Some (CTE c n); m p = Some (CTE c node); m' p' = Some (CTE c' n'); m p' = Some (CTE c' nodea); untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}; untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p'; descendants_of' p m \<subseteq> descendants_of' p m'; descendants_of' p' m \<subseteq> descendants_of' p' m'\<rbrakk> \<Longrightarrow> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m') \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m') \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal:
No subgoals! proof (state)
this:
untyped_inc' m \<longrightarrow> untyped_inc' m'

goal (1 subgoal):
 1. untyped_mdb' m \<longrightarrow> untyped_mdb' m' proof (prove)
goal (1 subgoal):
 1. \<And>x cte. m' x = Some cte \<Longrightarrow> \<exists>cap node. m x = Some (CTE cap node) \<and> isUntypedCap cap = isUntypedCap (cteCap cte) \<and> capRange cap = capRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte. \<lbrakk>m' x = Some cte; (m x = None) = (m' x = None) \<and> (\<forall>cte cte'. m x = Some cte \<and> m' x = Some cte' \<longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> capRange (cteCap cte) = capRange (cteCap cte') \<and> (isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = cteCap cte'))\<rbrakk> \<Longrightarrow> \<exists>cap node. m x = Some (CTE cap node) \<and> isUntypedCap cap = isUntypedCap (cteCap cte) \<and> capRange cap = capRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte y. \<lbrakk>m' x = Some cte; m x = Some y; isUntypedCap (cteCap y) = isUntypedCap (cteCap cte); capRange (cteCap y) = capRange (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap y = cteCap cte\<rbrakk> \<Longrightarrow> \<exists>cap. (\<exists>node. y = CTE cap node) \<and> isUntypedCap cap = isUntypedCap (cteCap cte) \<and> capRange cap = capRange (cteCap cte) proof (prove)
goal:
No subgoals! proof (state)
this:
m' ?x = Some ?cte \<Longrightarrow> \<exists>cap node. m ?x = Some (CTE cap node) \<and> isUntypedCap cap = isUntypedCap (cteCap ?cte) \<and> capRange cap = capRange (cteCap ?cte)

goal (1 subgoal):
 1. untyped_mdb' m \<longrightarrow> untyped_mdb' m' proof (prove)
goal (1 subgoal):
 1. untyped_mdb' m \<longrightarrow> untyped_mdb' m' proof (prove)
goal (1 subgoal):
 1. (\<forall>p p' c n c' n'. m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m p' = Some (CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<longrightarrow> (\<forall>p p' c n c' n'. m' p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m' p' = Some (CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m') proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<forall>c n c' n'. m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m p' = Some (CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m \<Longrightarrow> \<forall>c n c' n'. m' p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m' p' = Some (CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m' p = Some (CTE c n); isUntypedCap c; m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<exists>node. m p = Some (CTE (cteCap (CTE c n)) node) \<and> m' p = Some (CTE c n)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c'. \<lbrakk>\<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; (\<exists>node. m p = Some (CTE c node)) \<and> m' p = Some (CTE c n); \<exists>cap. (\<exists>node. m p' = Some (CTE cap node)) \<and> \<not> isUntypedCap cap \<and> capRange cap = capRange c'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' cap node nodea. \<lbrakk>p' \<in> descendants_of' p m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); m p = Some (CTE c node); m p' = Some (CTE cap nodea); \<not> isUntypedCap cap; capRange cap = capRange c'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' cap node nodea. \<lbrakk>p' \<in> descendants_of' p m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); m p = Some (CTE c node); m p' = Some (CTE cap nodea); \<not> isUntypedCap cap; capRange cap = capRange c'; descendants_of' p m \<subseteq> descendants_of' p m'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal:
No subgoals! proof (state)
this:
untyped_mdb' m \<longrightarrow> untyped_mdb' m'

goal:
No subgoals!