theory CSpace_AI

lemma (in mdb_insert_abs) untyped_mdb:
  assumes u: "untyped_mdb m cs"
  assumes src: "cs src = Some c"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes d: "is_derived m src cap c"
  shows "untyped_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" unfolding untyped_mdb_def apply (intro allI impI) apply (simp add: descendants_child) apply (rule conjI) apply (rule impI) apply (rule disjCI2) apply simp apply (case_tac "ptr = dest") apply simp apply (insert u)[1] apply (unfold untyped_mdb_def) apply (erule allE)+ apply (erule impE, rule src) apply (erule impE) apply (insert d) apply (clarsimp simp: is_cap_simps is_derived_def cap_master_cap_simps
                    split: cap.splits) apply (drule cap_master_cap_eqDs) apply fastforce apply (erule (1) impE) apply (erule impE) apply (clarsimp simp: is_cap_simps is_derived_def cap_master_cap_simps
                   split: if_split_asm cap.splits) apply (fastforce dest: cap_master_cap_eqDs) apply (simp add: descendants_of_def) apply (insert u)[1] apply (unfold untyped_mdb_def) apply fastforce apply (rule conjI) apply (rule impI) apply (rule disjCI2) apply (simp add: neq) apply (insert u src)[1] apply simp apply (unfold untyped_mdb_def) apply (erule allE)+ apply (erule impE, rule src) apply (erule impE) subgoal by (clarsimp simp: is_cap_simps is_derived_def same_object_as_def
                        split: cap.splits) apply (erule (1) impE) subgoal by simp apply (rule impI) apply (erule conjE) apply (simp split: if_split_asm) subgoal by (clarsimp simp: is_cap_simps) apply (insert u)[1] apply (unfold untyped_mdb_def) apply (erule allE)+ apply (erule impE, rule src) apply (erule impE) apply (clarsimp simp: is_cap_simps is_derived_def cap_master_cap_simps
                    split: cap.splits) apply (fastforce dest: cap_master_cap_eqDs) apply (erule (1) impE) apply (erule impE) apply (clarsimp simp: is_cap_simps is_derived_def cap_master_cap_simps
                    split: if_split_asm cap.splits) apply (fastforce dest: cap_master_cap_eqDs) apply (clarsimp simp: is_cap_simps is_derived_def cap_master_cap_simps
                   split: if_split_asm cap.splits) apply (fastforce dest: cap_master_cap_eqDs) apply (insert u)[1] apply (unfold untyped_mdb_def) apply (erule allE)+ apply (erule (1) impE) apply (erule (1) impE) apply (erule impE, rule src) apply (erule impE) apply (clarsimp simp:  is_derived_def
                   split: if_split_asm) apply (drule master_cap_obj_refs) apply (fastforce dest: master_cap_obj_refs) subgoal by (clarsimp simp:is_cap_simps cap_master_cap_def dest!: master_arch_cap_obj_refs split:cap.splits) subgoal by simp apply (insert u)[1] apply (unfold untyped_mdb_def) apply fastforce 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)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>(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>(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 (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>(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
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>(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> {}; src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>(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> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr = dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; untyped_mdb m cs\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; \<forall>ptr ptr' cap cap'. cs ptr = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> cs ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; cs (?ptr23 ptr ptr' capa cap') = Some (?cap27 ptr ptr' capa cap') \<longrightarrow> is_untyped_cap (?cap27 ptr ptr' capa cap') \<longrightarrow> cs (?ptr'25 ptr ptr' capa cap') = Some (?cap'29 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'29 ptr ptr' capa cap') \<inter> untyped_range (?cap27 ptr ptr' capa cap') \<noteq> {} \<longrightarrow> ?ptr'25 ptr ptr' capa cap' \<in> descendants_of (?ptr23 ptr ptr' capa cap') m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; is_untyped_cap c \<longrightarrow> cs (?ptr'25 ptr ptr' capa cap') = Some (?cap'29 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'29 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'25 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest\<rbrakk> \<Longrightarrow> is_untyped_cap c
 2. \<And>ptr ptr' capa cap'. \<lbrakk>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; cs (?ptr'25 ptr ptr' capa cap') = Some (?cap'29 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'29 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'25 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>(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> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> is_untyped_cap c
 2. \<And>ptr ptr' capa cap'. \<lbrakk>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; cs (?ptr'25 ptr ptr' capa cap') = Some (?cap'29 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'29 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'25 ptr ptr' capa cap' \<in> descendants_of src m; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>a b aa ba cap' dev r bits f. \<lbrakk>cs (aa, ba) = Some cap'; obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; src \<in> descendants_of (a, b) m; dest = (a, b); \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; cap = UntypedCap dev r bits f; \<forall>r b n. c \<noteq> Zombie r b n; \<forall>x R. c \<noteq> ReplyCap x True R; is_derived_arch (UntypedCap dev r bits f) c; \<forall>x R. c \<noteq> ReplyCap x False R; cap_master_cap c = UntypedCap dev r bits 0; cap_badge c = None\<rbrakk> \<Longrightarrow> aa = a \<and> ba = b
 2. \<And>ptr ptr' capa cap'. \<lbrakk>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; cs (?ptr'25 ptr ptr' capa cap') = Some (?cap'29 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'29 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'25 ptr ptr' capa cap' \<in> descendants_of src m; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>a b aa ba cap' dev r bits f. \<lbrakk>cs (aa, ba) = Some cap'; obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; src \<in> descendants_of (a, b) m; dest = (a, b); \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; cap = UntypedCap dev r bits f; \<forall>r b n. c \<noteq> Zombie r b n; \<forall>x R. c \<noteq> ReplyCap x True R; is_derived_arch (UntypedCap dev r bits f) c; \<forall>x R. c \<noteq> ReplyCap x False R; cap_badge c = None; \<exists>f. c = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> aa = a \<and> ba = b
 2. \<And>ptr ptr' capa cap'. \<lbrakk>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; cs (?ptr'25 ptr ptr' capa cap') = Some (?cap'29 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'29 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'25 ptr ptr' capa cap' \<in> descendants_of src m; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; cs (?ptr'25 ptr ptr' capa cap') = Some (?cap'29 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'29 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'25 ptr ptr' capa cap' \<in> descendants_of src m; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; is_derived m src cap c; obj_refs cap' \<inter> untyped_range c \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range c \<noteq> {}
 2. \<And>ptr ptr' capa cap'. \<lbrakk>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; is_derived m src cap c; ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>a b aa ba cap' dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; cs (aa, ba) = Some cap'; obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; src \<in> descendants_of (a, b) m; \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; dest = (a, b); \<forall>r b n. c \<noteq> Zombie r b n; cap_master_cap c = UntypedCap dev r bits 0; cap_badge c = None; \<forall>x R. c \<noteq> ReplyCap x True R; is_derived_arch (UntypedCap dev r bits f) c; \<forall>x R. c \<noteq> ReplyCap x False R; aa = a \<longrightarrow> ba \<noteq> b; obj_refs cap' \<inter> untyped_range c = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; is_derived m src cap c; ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>cap = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of dest m; ptr' \<noteq> dest; ptr = dest; is_derived m src cap c; ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c; untyped_mdb m cs\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>(if ptr = dest then Some cap else cs ptr) = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; is_derived m src cap c; \<forall>ptr ptr' cap cap'. cs ptr = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> cs ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> (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>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> ptr = src \<longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>(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> {}; is_derived m src cap c; ptr = src\<rbrakk> \<Longrightarrow> ptr' = dest \<or> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>(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> {}; is_derived m src cap c; ptr = src; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>cs src = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; ptr = src; ptr' \<noteq> dest\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>cs src = Some capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; ptr = src; ptr' \<noteq> dest; untyped_mdb m cs; cs src = Some c\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>c = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap capa; ptr = src; ptr' \<noteq> dest; untyped_mdb m cs; cs src = Some capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>c = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap capa; ptr = src; ptr' \<noteq> dest; \<forall>ptr ptr' cap cap'. cs ptr = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> cs ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m; cs src = Some capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>c = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap capa; ptr = src; ptr' \<noteq> dest; cs src = Some capa; cs (?ptr186 ptr ptr' capa cap') = Some (?cap190 ptr ptr' capa cap') \<longrightarrow> is_untyped_cap (?cap190 ptr ptr' capa cap') \<longrightarrow> cs (?ptr'188 ptr ptr' capa cap') = Some (?cap'192 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'192 ptr ptr' capa cap') \<inter> untyped_range (?cap190 ptr ptr' capa cap') \<noteq> {} \<longrightarrow> ?ptr'188 ptr ptr' capa cap' \<in> descendants_of (?ptr186 ptr ptr' capa cap') m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>c = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap capa; ptr = src; ptr' \<noteq> dest; cs src = Some capa; is_untyped_cap c \<longrightarrow> cs (?ptr'188 ptr ptr' capa cap') = Some (?cap'192 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'192 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'188 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>c = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap capa; ptr = src; ptr' \<noteq> dest; cs src = Some capa\<rbrakk> \<Longrightarrow> is_untyped_cap c
 2. \<And>ptr ptr' capa cap'. \<lbrakk>c = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap capa; ptr = src; ptr' \<noteq> dest; cs src = Some capa; cs (?ptr'188 ptr ptr' capa cap') = Some (?cap'192 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'192 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'188 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = capa_; is_untyped_cap capa_; cs ptr'_ = Some cap'_; obj_refs cap'_ \<inter> untyped_range capa_ \<noteq> {}; is_derived m src cap capa_; ptr_ = src; ptr'_ \<noteq> dest; cs src = Some capa_\<rbrakk> \<Longrightarrow> is_untyped_cap c proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>c = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap capa; ptr = src; ptr' \<noteq> dest; cs src = Some capa; cs (?ptr'188 ptr ptr' capa cap') = Some (?cap'192 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'192 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'188 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>c = capa; is_untyped_cap capa; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap capa; ptr = src; ptr' \<noteq> dest; cs src = Some capa; obj_refs cap' \<inter> untyped_range c \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of src m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = capa_; is_untyped_cap capa_; cs ptr'_ = Some cap'_; obj_refs cap'_ \<inter> untyped_range capa_ \<noteq> {}; is_derived m src cap capa_; ptr_ = src; ptr'_ \<noteq> dest; cs src = Some capa_; obj_refs cap'_ \<inter> untyped_range c \<noteq> {} \<longrightarrow> ptr'_ \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr'_ \<in> descendants_of src m proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c\<rbrakk> \<Longrightarrow> 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>(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> {}; is_derived m src cap c; src \<notin> descendants_of ptr m \<and> ptr \<noteq> src\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>(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> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range cap' \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = cap'; is_untyped_cap cap'; ptr' = dest; capa = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_refs cap'_ \<inter> untyped_range cap'_ \<noteq> {}; is_derived m src cap'_ c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr_ = dest; cap = cap'_; is_untyped_cap cap'_; ptr'_ = dest; capa_ = cap'_\<rbrakk> \<Longrightarrow> dest \<in> descendants_of dest m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; untyped_mdb m cs\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; \<forall>ptr ptr' cap cap'. cs ptr = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> cs ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; cs (?ptr243 ptr ptr' capa cap') = Some (?cap247 ptr ptr' capa cap') \<longrightarrow> is_untyped_cap (?cap247 ptr ptr' capa cap') \<longrightarrow> cs (?ptr'245 ptr ptr' capa cap') = Some (?cap'249 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'249 ptr ptr' capa cap') \<inter> untyped_range (?cap247 ptr ptr' capa cap') \<noteq> {} \<longrightarrow> ?ptr'245 ptr ptr' capa cap' \<in> descendants_of (?ptr243 ptr ptr' capa cap') m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; is_untyped_cap c \<longrightarrow> cs (?ptr'245 ptr ptr' capa cap') = Some (?cap'249 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'249 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'245 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> is_untyped_cap c
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; cs (?ptr'245 ptr ptr' capa cap') = Some (?cap'249 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'249 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'245 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba cap' dev r bits f. \<lbrakk>obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; src \<notin> descendants_of (a, b) m; (a, b) \<noteq> src; cs (aa, ba) = Some cap'; dest = (a, b); \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; cap = UntypedCap dev r bits f; \<forall>r b n. c \<noteq> Zombie r b n; \<forall>x R. c \<noteq> ReplyCap x True R; is_derived_arch (UntypedCap dev r bits f) c; \<forall>x R. c \<noteq> ReplyCap x False R; cap_master_cap c = UntypedCap dev r bits 0; cap_badge c = None\<rbrakk> \<Longrightarrow> aa = a \<and> ba = b
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; cs (?ptr'245 ptr ptr' capa cap') = Some (?cap'249 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'249 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'245 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; cs (?ptr'245 ptr ptr' capa cap') = Some (?cap'249 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'249 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'245 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range c \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range c \<noteq> {}
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba cap' dev r bits f. \<lbrakk>src \<notin> descendants_of (a, b) m; (a, b) \<noteq> src; cap = UntypedCap dev r bits f; cs (aa, ba) = Some cap'; obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; dest = (a, b); \<forall>r b n. c \<noteq> Zombie r b n; cap_master_cap c = UntypedCap dev r bits 0; cap_badge c = None; \<forall>x R. c \<noteq> ReplyCap x True R; is_derived_arch (UntypedCap dev r bits f) c; \<forall>x R. c \<noteq> ReplyCap x False R; aa = a \<longrightarrow> ba \<noteq> b; obj_refs cap' \<inter> untyped_range c = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src capa c; src \<notin> descendants_of dest m; dest \<noteq> src; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; ptr' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba cap' dev r bits f. \<lbrakk>src \<notin> descendants_of (a, b) m; (a, b) \<noteq> src; cap = UntypedCap dev r bits f; cs (aa, ba) = Some cap'; (aa, ba) \<in> descendants_of src m; obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; dest = (a, b); (aa, ba) \<notin> descendants_of (a, b) m; \<forall>r b n. c \<noteq> Zombie r b n; cap_master_cap c = UntypedCap dev r bits 0; cap_badge c = None; \<forall>x R. c \<noteq> ReplyCap x True R; is_derived_arch (UntypedCap dev r bits f) c; \<forall>x R. c \<noteq> ReplyCap x False R\<rbrakk> \<Longrightarrow> aa = a \<and> ba = b
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; untyped_mdb m cs\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; \<forall>ptr ptr' cap cap'. cs ptr = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> cs ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; cs (?ptr436 ptr ptr' capa cap') = Some (?cap440 ptr ptr' capa cap') \<longrightarrow> is_untyped_cap (?cap440 ptr ptr' capa cap') \<longrightarrow> cs (?ptr'438 ptr ptr' capa cap') = Some (?cap'442 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'442 ptr ptr' capa cap') \<inter> untyped_range (?cap440 ptr ptr' capa cap') \<noteq> {} \<longrightarrow> ?ptr'438 ptr ptr' capa cap' \<in> descendants_of (?ptr436 ptr ptr' capa cap') m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; is_untyped_cap capa \<longrightarrow> cs (?ptr'438 ptr ptr' capa cap') = Some (?cap'442 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'442 ptr ptr' capa cap') \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ?ptr'438 ptr ptr' capa cap' \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; cs (?ptr'438 ptr ptr' capa cap') = Some (?cap'442 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'442 ptr ptr' capa cap') \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ?ptr'438 ptr ptr' capa cap' \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; obj_refs c \<inter> untyped_range capa \<noteq> {} \<longrightarrow> src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'\<rbrakk> \<Longrightarrow> obj_refs c \<inter> untyped_range capa \<noteq> {}
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba capa. \<lbrakk>src \<notin> descendants_of (a, b) m; (a, b) \<noteq> src; cs (a, b) = Some capa; is_untyped_cap capa; obj_refs cap \<inter> untyped_range capa \<noteq> {}; is_untyped_cap c; dest = (aa, ba); cap \<noteq> NullCap; \<not> is_zombie c; cap \<noteq> IRQControlCap; cap_master_cap c = cap_master_cap cap; descendants_of src m = {}; is_master_reply_cap c = is_reply_cap cap; is_derived_arch cap c; \<not> is_reply_cap c; \<not> is_master_reply_cap cap; a = aa \<longrightarrow> b \<noteq> ba; obj_refs c \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa ba capa. \<lbrakk>src \<notin> descendants_of (a, b) m; (a, b) \<noteq> src; cs (a, b) = Some capa; is_untyped_cap capa; obj_refs cap \<inter> untyped_range capa \<noteq> {}; \<not> is_untyped_cap c; dest = (aa, ba); cap \<noteq> NullCap; \<not> is_zombie c; cap \<noteq> IRQControlCap; cap_master_cap c = cap_master_cap cap; (cap_badge c, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap c = is_reply_cap cap; is_derived_arch cap c; \<not> is_reply_cap c; \<not> is_master_reply_cap cap; a = aa \<longrightarrow> b \<noteq> ba; obj_refs c \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba capa. \<lbrakk>src \<notin> descendants_of (a, b) m; (a, b) \<noteq> src; cs (a, b) = Some capa; is_untyped_cap capa; obj_refs cap \<inter> untyped_range capa \<noteq> {}; is_untyped_cap c; dest = (aa, ba); cap \<noteq> NullCap; \<not> is_zombie c; cap \<noteq> IRQControlCap; descendants_of src m = {}; is_master_reply_cap c = is_reply_cap cap; is_derived_arch cap c; \<not> is_reply_cap c; \<not> is_master_reply_cap cap; a = aa \<longrightarrow> b \<noteq> ba; obj_refs c \<inter> untyped_range capa = {}; obj_refs c = obj_refs cap\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa ba capa. \<lbrakk>src \<notin> descendants_of (a, b) m; (a, b) \<noteq> src; cs (a, b) = Some capa; is_untyped_cap capa; obj_refs cap \<inter> untyped_range capa \<noteq> {}; \<not> is_untyped_cap c; dest = (aa, ba); cap \<noteq> NullCap; \<not> is_zombie c; cap \<noteq> IRQControlCap; cap_master_cap c = cap_master_cap cap; (cap_badge c, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap c = is_reply_cap cap; is_derived_arch cap c; \<not> is_reply_cap c; \<not> is_master_reply_cap cap; a = aa \<longrightarrow> b \<noteq> ba; obj_refs c \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 4. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba capa. \<lbrakk>src \<notin> descendants_of (a, b) m; (a, b) \<noteq> src; cs (a, b) = Some capa; is_untyped_cap capa; obj_refs cap \<inter> untyped_range capa \<noteq> {}; \<not> is_untyped_cap c; dest = (aa, ba); cap \<noteq> NullCap; \<not> is_zombie c; cap \<noteq> IRQControlCap; cap_master_cap c = cap_master_cap cap; (cap_badge c, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap c = is_reply_cap cap; is_derived_arch cap c; \<not> is_reply_cap c; \<not> is_master_reply_cap cap; a = aa \<longrightarrow> b \<noteq> ba; obj_refs c \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 3. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src \<notin> descendants_of (a_, b_) m; (a_, b_) \<noteq> src; cs (a_, b_) = Some capa_; is_untyped_cap capa_; obj_refs cap \<inter> untyped_range capa_ \<noteq> {}; \<not> is_untyped_cap c; dest = (aa_, ba_); cap \<noteq> NullCap; \<not> is_zombie c; cap \<noteq> IRQControlCap; cap_master_cap c = cap_master_cap cap; (cap_badge c, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap c = is_reply_cap cap; is_derived_arch cap c; \<not> is_reply_cap c; \<not> is_master_reply_cap cap; a_ = aa_ \<longrightarrow> b_ \<noteq> ba_; obj_refs c \<inter> untyped_range capa_ = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap' c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m
 2. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_refs cap'_ \<inter> untyped_range capa_ \<noteq> {}; is_derived m src cap'_ c; src \<notin> descendants_of ptr_ m; ptr_ \<noteq> src; ptr_ \<noteq> dest; cs ptr_ = Some capa_; is_untyped_cap capa_; ptr'_ = dest; cap = cap'_; src \<in> descendants_of ptr_ m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr_ m proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; untyped_mdb m cs\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>obj_refs cap' \<inter> untyped_range capa \<noteq> {}; is_derived m src cap c; src \<notin> descendants_of ptr m; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; \<forall>ptr ptr' cap cap'. cs ptr = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> cs ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal:
No subgoals!