theory Detype_AI

lemma (in Detype_AI) untyped_cap_descendants_range:
  "\<lbrakk>valid_pspace (s :: 'a state); caps_of_state s p = Some cap; is_untyped_cap cap;valid_mdb s;
   q\<in> descendants_of p (cdt s) \<rbrakk>
   \<Longrightarrow>  cte_wp_at (\<lambda>c. (cap_range c \<inter> usable_untyped_range cap = {})) q s" apply (clarsimp simp: valid_pspace_def) apply (frule(1) descendants_of_cte_at) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (case_tac "is_untyped_cap capa") apply (frule(1) valid_cap_aligned[OF caps_of_state_valid]) apply (frule_tac cap = capa in valid_cap_aligned[OF caps_of_state_valid]) apply simp apply (frule_tac c = capa in untyped_range_non_empty) apply simp apply (frule_tac c = cap in untyped_range_non_empty) apply simp apply (clarsimp simp:valid_mdb_def) apply (drule untyped_incD) apply simp+ apply clarify apply (erule subset_splitE) apply simp apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (clarsimp simp:descendants_of_def) apply (drule(1) trancl_trans) apply (simp add:vmdb_abs_def valid_mdb_def vmdb_abs.no_loops) apply simp apply simp apply (clarsimp simp:descendants_of_def | erule disjE)+ apply (drule(1) trancl_trans) apply (simp add:vmdb_abs_def valid_mdb_def vmdb_abs.no_loops)+ apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (erule(1) disjoint_subset2[OF usable_range_subseteq]) apply (simp add:Int_ac) apply (drule(1) caps_of_state_valid)+ apply (frule_tac cap = capa in caps_of_state_ko) apply (elim disjE) apply clarsimp+ apply (clarsimp simp:valid_cap_def is_cap_simps valid_untyped_def
             simp del:usable_untyped_range.simps untyped_range.simps) apply (rule ccontr) apply (clarsimp dest!: int_not_emptyD simp del:usable_untyped_range.simps untyped_range.simps) apply (thin_tac "\<forall>x y z. P x y z" for P) apply (drule(1) bspec) apply (clarsimp dest!: int_not_emptyD simp del:usable_untyped_range.simps untyped_range.simps) apply (drule_tac x = x in spec) apply (clarsimp simp del:usable_untyped_range.simps untyped_range.simps) apply (drule(2) p_in_obj_range ) apply (erule impE) apply (erule(1) notemptyI[OF IntI[OF _ subsetD[OF usable_range_subseteq]]]) apply (simp add:is_cap_simps) apply assumption apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace s; caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> usable_untyped_range cap = {}) q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> usable_untyped_range cap = {}) q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cte_wp_at (\<lambda>_. True) q s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> usable_untyped_range cap = {}) q s proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa\<rbrakk> \<Longrightarrow> cap_aligned capa
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}\<rbrakk> \<Longrightarrow> cap_aligned cap
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (6 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> caps_of_state s (?p'32 capa) = Some (?c'32 capa)
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> is_untyped_cap (?c'32 capa)
 4. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_inc (?m32 capa) (caps_of_state s)
 5. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (untyped_range cap \<subseteq> untyped_range (?c'32 capa) \<or> untyped_range (?c'32 capa) \<subseteq> untyped_range cap \<or> untyped_range cap \<inter> untyped_range (?c'32 capa) = {}) \<and> (untyped_range cap \<subset> untyped_range (?c'32 capa) \<longrightarrow> p \<in> descendants_of (?p'32 capa) (?m32 capa) \<and> untyped_range cap \<inter> usable_untyped_range (?c'32 capa) = {}) \<and> (untyped_range (?c'32 capa) \<subset> untyped_range cap \<longrightarrow> ?p'32 capa \<in> descendants_of p (?m32 capa) \<and> untyped_range (?c'32 capa) \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap = untyped_range (?c'32 capa) \<longrightarrow> ?p'32 capa \<in> descendants_of p (?m32 capa) \<and> usable_untyped_range cap = {} \<or> p \<in> descendants_of (?p'32 capa) (?m32 capa) \<and> usable_untyped_range (?c'32 capa) = {} \<or> p = ?p'32 capa)\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 6. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (untyped_range cap \<subseteq> untyped_range capa \<or> untyped_range capa \<subseteq> untyped_range cap \<or> untyped_range cap \<inter> untyped_range capa = {}) \<and> (untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}) \<and> (untyped_range capa \<subset> untyped_range cap \<longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q)\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subseteq> untyped_range capa \<or> untyped_range capa \<subseteq> untyped_range cap \<or> untyped_range cap \<inter> untyped_range capa = {}; untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (5 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<subset> untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range capa \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap = untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 4. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 5. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (5 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<subset> untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range capa \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap = untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 4. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 5. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (5 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<subset> untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range capa \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap = untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 4. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 5. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (5 subgoals):
 1. \<And>capa x. \<lbrakk>is_untyped_cap cap; cdt s \<Turnstile> p \<rightarrow> q; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<subseteq> untyped_range capa; untyped_range capa \<inter> usable_untyped_range cap \<noteq> {}; x \<in> untyped_range capa; cdt s \<Turnstile> q \<rightarrow> p; untyped_range cap \<inter> usable_untyped_range capa = {}\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range capa \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap = untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 4. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 5. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (5 subgoals):
 1. \<And>capa x. \<lbrakk>is_untyped_cap cap; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<subseteq> untyped_range capa; untyped_range capa \<inter> usable_untyped_range cap \<noteq> {}; x \<in> untyped_range capa; cdt s \<Turnstile> q \<rightarrow> p; untyped_range cap \<inter> usable_untyped_range capa = {}; cdt s \<Turnstile> p \<rightarrow> p\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range capa \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap = untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 4. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 5. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (4 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range capa \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap = untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 4. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap = untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; untyped_range cap = untyped_range capa\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (4 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; cdt s \<Turnstile> p \<rightarrow> q; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap = untyped_range capa; cdt s \<Turnstile> q \<rightarrow> p; usable_untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; cdt s \<Turnstile> p \<rightarrow> q; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap = untyped_range capa; p = q\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 4. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (4 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap = untyped_range capa; cdt s \<Turnstile> q \<rightarrow> p; usable_untyped_range capa = {}; cdt s \<Turnstile> p \<rightarrow> p\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; cdt s \<Turnstile> p \<rightarrow> q; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap = untyped_range capa; p = q\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 4. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<subset> untyped_range capa \<longrightarrow> p \<in> descendants_of q (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range capa = {}; untyped_range cap = untyped_range capa \<longrightarrow> usable_untyped_range cap = {} \<or> p \<in> descendants_of q (cdt s) \<and> usable_untyped_range capa = {} \<or> p = q; \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned cap; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; is_untyped_cap capa; cap_aligned capa; untyped_range capa \<noteq> {}; untyped_range cap \<noteq> {}; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<not> untyped_range capa \<subset> untyped_range cap; untyped_range cap \<inter> untyped_range capa = {}\<rbrakk> \<Longrightarrow> untyped_range capa \<inter> untyped_range cap = {}
 2. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s q = Some capa; \<not> is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<not> is_untyped_cap capa; s \<turnstile> cap; s \<turnstile> capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<not> is_untyped_cap capa; s \<turnstile> cap; s \<turnstile> capa; is_untyped_cap capa \<or> cap_range capa = {} \<or> (\<forall>ptr\<in>cap_range capa. \<exists>ko. kheap s ptr = Some ko)\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<not> is_untyped_cap capa; s \<turnstile> cap; s \<turnstile> capa; is_untyped_cap capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 2. \<And>capa. \<lbrakk>is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<not> is_untyped_cap capa; s \<turnstile> cap; s \<turnstile> capa; cap_range capa = {}\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {}
 3. \<And>capa. \<lbrakk>is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<not> is_untyped_cap capa; s \<turnstile> cap; s \<turnstile> capa; \<forall>ptr\<in>cap_range capa. \<exists>ko. kheap s ptr = Some ko\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>is_untyped_cap cap; valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<not> is_untyped_cap capa; s \<turnstile> cap; s \<turnstile> capa; \<forall>ptr\<in>cap_range capa. \<exists>ko. kheap s ptr = Some ko\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range cap = {} proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f; \<forall>ptr\<in>cap_range capa. \<exists>ko. kheap s ptr = Some ko; cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> cap_range capa \<inter> usable_untyped_range (UntypedCap dev r bits f) = {} proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f; \<forall>ptr\<in>cap_range capa. \<exists>ko. kheap s ptr = Some ko; cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; cap_range capa \<inter> usable_untyped_range (UntypedCap dev r bits f) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f x. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f; \<forall>ptr\<in>cap_range capa. \<exists>ko. kheap s ptr = Some ko; cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f x. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<forall>ptr\<in>cap_range capa. \<exists>ko. kheap s ptr = Some ko; cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f x. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); \<exists>ko. kheap s x = Some ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); kheap s x = Some ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); kheap s x = Some ko; \<forall>obj. kheap s x = Some obj \<longrightarrow> obj_range x obj \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range x obj \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range x obj = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); kheap s x = Some ko; obj_range x ko \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range x ko \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); obj_range x ko \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {} \<longrightarrow> obj_range x ko \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range x ko = {}; x \<in> obj_range x ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); x \<in> obj_range x ko\<rbrakk> \<Longrightarrow> obj_range x ko \<inter> untyped_range (UntypedCap dev r bits f) \<noteq> {}
 2. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); x \<in> obj_range x ko; obj_range x ko \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap dev r bits f)
 2. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> x \<in> usable_untyped_range (UntypedCap dev r bits f)
 3. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); x \<in> obj_range x ko; obj_range x ko \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> x \<in> usable_untyped_range (UntypedCap dev r bits f)
 2. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); x \<in> obj_range x ko; obj_range x ko \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>capa dev r bits f x ko. \<lbrakk>valid_mdb s; q \<in> descendants_of p (cdt s); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); cap = UntypedCap dev r bits f; cap_aligned (UntypedCap dev r bits f); cap_aligned capa; case capa of UntypedCap dev p b f \<Rightarrow> valid_untyped capa s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; x \<in> cap_range capa; x \<in> usable_untyped_range (UntypedCap dev r bits f); x \<in> obj_range x ko; obj_range x ko \<subseteq> untyped_range (UntypedCap dev r bits f) \<and> usable_untyped_range (UntypedCap dev r bits f) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!