theory Detype_AI

lemma (in Detype_AI) cte_map_not_null_outside: (*FIXME: arch_split*)
  "\<lbrakk> cte_wp_at ((\<noteq>) cap.NullCap) p (s :: 'a state);
     cte_wp_at ((=) cap) p' s;is_untyped_cap cap;
     descendants_range cap p' s; untyped_children_in_mdb s;
     if_unsafe_then_cap s; valid_global_refs s \<rbrakk>
     \<Longrightarrow> fst p \<notin> untyped_range cap" apply (simp add:descendants_range_def2) apply (case_tac "cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s") apply (rule ccontr) apply (erule(2) untyped_children_in_mdbEE[where ptr'=p]) apply (simp add:cte_wp_at_caps_of_state is_cap_simps) apply (clarsimp simp:cte_wp_at_caps_of_state is_cap_simps) apply (drule descendants_range_inD) apply (simp add:cte_wp_at_caps_of_state) apply (simp add:cte_wp_at_caps_of_state) apply simp apply (drule(1) if_unsafe_then_capD, simp) apply (drule ex_cte_cap_to_obj_ref_disj, erule disjE) apply (clarsimp simp del:untyped_range.simps)+ apply (erule(1) untyped_children_in_mdbEE [where P="\<lambda>c. fst p \<in> f c" for f]) apply simp+ apply fastforce apply (drule(1) descendants_range_inD) apply (simp add:cte_wp_at_caps_of_state) apply simp apply clarsimp apply (drule(1) valid_globals_irq_node, fastforce simp: cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range cap p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap
 2. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> cte_wp_at ?P4 p s
 2. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; ?P4 cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {}
 3. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; NullCap \<noteq> cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {}
 2. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> ?p'24 cap' \<in> descendants_of p' (cdt s)
 2. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> caps_of_state s (?p'24 cap') = Some (?cap24 cap')
 3. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s); cap_range (?cap24 cap') \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> caps_of_state s p = Some (?cap24 cap')
 2. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s); cap_range (?cap24 cap') \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap'. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<not> fst p \<notin> untyped_range cap; cte_wp_at ((=) cap') p s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; p \<in> descendants_of p' (cdt s); cap_range cap' \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. NullCap \<noteq> cap' \<and> appropriate_cte_cap cap' cap) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr'. cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) ptr' s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap
 2. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. fst p \<in> ?f46 a b c) (?ptr'43 a b) s
 3. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap; cte_wp_at ((=) cap') (?ptr'43 a b) s; fst p \<in> ?f46 a b cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {}
 4. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap; cte_wp_at ((=) cap') (?ptr'43 a b) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; ?ptr'43 a b \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap; cte_wp_at ((=) cap') (a, b) s; fst p \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {}
 2. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = Some (?cap59 a b cap')
 2. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s); cap_range (?cap59 a b cap') \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> untyped_range cap; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s); cap_range cap' \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = fst p) p s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>a b irq. \<lbrakk>cte_wp_at ((=) cap) p' s; is_untyped_cap cap; descendants_range_in (untyped_range cap) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; \<not> cte_wp_at (\<lambda>c. is_zombie c \<and> obj_ref_of c = interrupt_irq_node s irq) (interrupt_irq_node s irq, []) s; cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s; p = (interrupt_irq_node s irq, []); interrupt_irq_node s irq \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!