theory CSpace_AI

lemma (in mdb_insert_abs_sib) untyped_mdb_sib:
  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 n (cs(dest \<mapsto> cap))" unfolding untyped_mdb_def apply (intro allI impI) apply (simp add: descendants) apply (rule conjI) apply (rule impI, rule disjCI) apply (simp split: if_split_asm) 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 (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 (simp add: descendants_of_def) apply (insert u)[1] apply (unfold untyped_mdb_def) apply fastforce apply (rule impI) apply (simp split: if_split_asm) apply (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) apply (fastforce dest: cap_master_cap_eqDs) apply (clarsimp simp: is_cap_simps is_derived_def cap_master_cap_simps
                   split: if_split_asm) 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_cap_simps is_derived_def cap_master_cap_simps
                   split: if_split_asm cap.splits dest!:cap_master_cap_eqDs) apply (blast dest: master_cap_obj_refs) apply simp apply (insert u)[1] apply (unfold untyped_mdb_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb n (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 n 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 n 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' \<in> descendants_of ptr m \<or> ptr' = dest) \<and> (src \<notin> descendants_of ptr m \<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' \<in> descendants_of ptr m \<or> ptr' = dest
 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> src \<notin> descendants_of ptr m \<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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' cap cap'. \<lbrakk>is_untyped_cap cap; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; cs ptr = Some cap\<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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; untyped_mdb m cs\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' cap cap'. \<lbrakk>is_untyped_cap cap; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; cs ptr = Some cap\<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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; \<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' cap cap'. \<lbrakk>is_untyped_cap cap; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; cs ptr = Some cap\<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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; cs (?ptr33 ptr ptr' capa cap') = Some (?cap37 ptr ptr' capa cap') \<longrightarrow> is_untyped_cap (?cap37 ptr ptr' capa cap') \<longrightarrow> cs (?ptr'35 ptr ptr' capa cap') = Some (?cap'39 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'39 ptr ptr' capa cap') \<inter> untyped_range (?cap37 ptr ptr' capa cap') \<noteq> {} \<longrightarrow> ?ptr'35 ptr ptr' capa cap' \<in> descendants_of (?ptr33 ptr ptr' capa cap') m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' cap cap'. \<lbrakk>is_untyped_cap cap; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; cs ptr = Some cap\<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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; is_untyped_cap c \<longrightarrow> cs (?ptr'35 ptr ptr' capa cap') = Some (?cap'39 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'39 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'35 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 2. \<And>ptr ptr' cap cap'. \<lbrakk>is_untyped_cap cap; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; cs ptr = Some cap\<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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa\<rbrakk> \<Longrightarrow> is_untyped_cap c
 2. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; cs (?ptr'35 ptr ptr' capa cap') = Some (?cap'39 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'39 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'35 ptr ptr' capa cap' \<in> descendants_of src m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of dest m
 3. \<And>ptr ptr' cap cap'. \<lbrakk>is_untyped_cap cap; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; src \<in> descendants_of ptr m; ptr' \<noteq> dest; ptr \<noteq> dest; cs ptr = Some cap\<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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; is_derived m src cap c\<rbrakk> \<Longrightarrow> is_untyped_cap c
 2. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; cs (?ptr'35 ptr ptr' capa cap') = Some (?cap'39 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'39 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'35 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>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<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>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; cap = capa; cs (?ptr'35 ptr ptr' capa cap') = Some (?cap'39 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'39 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'35 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>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; cs (?ptr'35 ptr ptr' capa cap') = Some (?cap'39 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'39 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'35 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>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; 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>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (4 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; is_derived m src cap c\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range c \<noteq> {}
 2. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; 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>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<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; cap = UntypedCap dev r bits f; \<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>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; cap = capa; 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>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cap = capa; 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>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' capa cap'. \<lbrakk>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; cs ptr = Some capa; 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> src \<notin> descendants_of ptr m \<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> src \<notin> descendants_of ptr m \<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\<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; 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; 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> 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> 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; 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> 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> 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; 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> 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> 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; 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> 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> 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; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; cs (?ptr251 ptr ptr' capa cap') = Some (?cap255 ptr ptr' capa cap') \<longrightarrow> is_untyped_cap (?cap255 ptr ptr' capa cap') \<longrightarrow> cs (?ptr'253 ptr ptr' capa cap') = Some (?cap'257 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'257 ptr ptr' capa cap') \<inter> untyped_range (?cap255 ptr ptr' capa cap') \<noteq> {} \<longrightarrow> ?ptr'253 ptr ptr' capa cap' \<in> descendants_of (?ptr251 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> 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> 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; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; is_untyped_cap c \<longrightarrow> cs (?ptr'253 ptr ptr' capa cap') = Some (?cap'257 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'257 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'253 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> 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> 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; 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; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; cs (?ptr'253 ptr ptr' capa cap') = Some (?cap'257 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'257 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'253 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> 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> 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; 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; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; cs (?ptr'253 ptr ptr' capa cap') = Some (?cap'257 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'257 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'253 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> 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> 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; ptr = dest; cap = capa; is_untyped_cap capa; ptr' \<noteq> dest; cs ptr' = Some cap'; cs (?ptr'253 ptr ptr' capa cap') = Some (?cap'257 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'257 ptr ptr' capa cap') \<inter> untyped_range c \<noteq> {} \<longrightarrow> ?ptr'253 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> 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> 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; 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> 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> 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; 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; 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> 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> 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; 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; 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> 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> 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; 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> 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> 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; 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> 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> 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> 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> 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> 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> 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> 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> 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> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; cs (?ptr444 ptr ptr' capa cap') = Some (?cap448 ptr ptr' capa cap') \<longrightarrow> is_untyped_cap (?cap448 ptr ptr' capa cap') \<longrightarrow> cs (?ptr'446 ptr ptr' capa cap') = Some (?cap'450 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'450 ptr ptr' capa cap') \<inter> untyped_range (?cap448 ptr ptr' capa cap') \<noteq> {} \<longrightarrow> ?ptr'446 ptr ptr' capa cap' \<in> descendants_of (?ptr444 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> 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> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; is_untyped_cap capa \<longrightarrow> cs (?ptr'446 ptr ptr' capa cap') = Some (?cap'450 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'450 ptr ptr' capa cap') \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ?ptr'446 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> 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> dest; cs ptr = Some capa; is_untyped_cap capa; ptr' = dest; cap = cap'; cs (?ptr'446 ptr ptr' capa cap') = Some (?cap'450 ptr ptr' capa cap') \<longrightarrow> obj_refs (?cap'450 ptr ptr' capa cap') \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ?ptr'446 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> 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> 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> 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> 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> 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> 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 dev r bits f. \<lbrakk>src \<notin> descendants_of (a, b) m; cs (a, b) = Some (UntypedCap dev r bits f); obj_refs cap \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; dest = (aa, ba); cap \<noteq> NullCap; \<forall>r b n. c \<noteq> Zombie r b n; cap \<noteq> IRQControlCap; cap_master_cap c = cap_master_cap cap; (cap_badge c, cap_badge cap) \<in> capBadge_ordering False; (\<exists>x R. c = ReplyCap x True R) = (\<exists>x R. cap = ReplyCap x False R); is_derived_arch cap c; \<forall>x R. c \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; a = aa \<longrightarrow> b \<noteq> ba; obj_refs c \<inter> {r..r + 2 ^ bits - 1} = {}\<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> 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> 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> 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> 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> 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> 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> 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!