theory Untyped_AI

lemma set_untyped_cap_caps_overlap_reserved:
  "\<lbrace>\<lambda>s. invs s \<and> S \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and>
  usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {} \<and>
  descendants_range_in S cref s \<and> cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s\<rbrace>
  set_cap (UntypedCap dev ptr sz idx') cref
 \<lbrace>\<lambda>rv s. caps_overlap_reserved S s\<rbrace>" apply (unfold caps_overlap_reserved_def) apply wp apply (clarsimp simp: cte_wp_at_caps_of_state caps_overlap_reserved_def
              simp del: usable_untyped_range.simps split: if_split_asm) apply (frule invs_mdb) apply (erule ranE) apply (simp split: if_split_asm del: usable_untyped_range.simps add: valid_mdb_def) apply (drule untyped_incD) apply ((simp add: is_cap_simps)+)[4] apply clarify apply (erule subset_splitE) apply (simp del: usable_untyped_range.simps) apply (thin_tac "P \<longrightarrow> Q" for P Q)+ apply (elim conjE) apply blast apply (simp del: usable_untyped_range.simps) apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (elim conjE) apply (drule(2) descendants_range_inD) apply simp apply (drule_tac B = S in disjoint_subset[rotated,OF _ usable_range_subseteq]) apply (rule valid_cap_aligned) apply (erule(1) caps_of_state_valid) apply simp+ apply (elim disjE) apply clarsimp apply (drule(2) descendants_range_inD) apply simp apply (drule_tac B=S in  disjoint_subset[rotated,OF _ usable_range_subseteq]) apply (rule valid_cap_aligned) apply (erule(1) caps_of_state_valid) apply simp+ apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (rule disjoint_subset[OF usable_range_subseteq]) apply (rule valid_cap_aligned) apply (erule(1) caps_of_state_valid) apply simp+ apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> S \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {} \<and> descendants_range_in S cref s \<and> cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s\<rbrace> set_cap (UntypedCap dev ptr sz idx') cref \<lbrace>\<lambda>rv. caps_overlap_reserved S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> S \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {} \<and> descendants_range_in S cref s \<and> cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s\<rbrace> set_cap (UntypedCap dev ptr sz idx') cref \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> S \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {} \<and> descendants_range_in S cref s \<and> cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s \<Longrightarrow> \<forall>cap\<in>ran ((caps_of_state s)(cref \<mapsto> UntypedCap dev ptr sz idx')). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>cap \<in> ran (\<lambda>a. if a = cref then Some (UntypedCap dev ptr sz idx') else caps_of_state s a); invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; caps_of_state s cref = Some (UntypedCap dev ptr sz idx); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>cap \<in> ran (\<lambda>a. if a = cref then Some (UntypedCap dev ptr sz idx') else caps_of_state s a); invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; caps_of_state s cref = Some (UntypedCap dev ptr sz idx); is_untyped_cap cap; valid_mdb s\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap x. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; caps_of_state s cref = Some (UntypedCap dev ptr sz idx); is_untyped_cap cap; valid_mdb s; (if x = cref then Some (UntypedCap dev ptr sz idx') else caps_of_state s x) = Some cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap x. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; caps_of_state s cref = Some (UntypedCap dev ptr sz idx); is_untyped_cap cap; x \<noteq> cref; 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); caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s cap x. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; x \<noteq> cref; 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); caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap dev ptr sz idx)
 2. \<And>s cap x. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; x \<noteq> cref; 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); caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> caps_of_state s (?p'43 s cap x) = Some (?c'43 s cap x)
 3. \<And>s cap x. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; x \<noteq> cref; 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); caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> is_untyped_cap (?c'43 s cap x)
 4. \<And>s cap x. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; x \<noteq> cref; 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); caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> untyped_inc (?m43 s cap x) (caps_of_state s)
 5. \<And>s cap x. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; x \<noteq> cref; 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); caps_of_state s x = Some cap; (untyped_range (UntypedCap dev ptr sz idx) \<subseteq> untyped_range (?c'43 s cap x) \<or> untyped_range (?c'43 s cap x) \<subseteq> untyped_range (UntypedCap dev ptr sz idx) \<or> untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range (?c'43 s cap x) = {}) \<and> (untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range (?c'43 s cap x) \<longrightarrow> cref \<in> descendants_of (?p'43 s cap x) (?m43 s cap x) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range (?c'43 s cap x) = {}) \<and> (untyped_range (?c'43 s cap x) \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> ?p'43 s cap x \<in> descendants_of cref (?m43 s cap x) \<and> untyped_range (?c'43 s cap x) \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}) \<and> (untyped_range (UntypedCap dev ptr sz idx) = untyped_range (?c'43 s cap x) \<longrightarrow> ?p'43 s cap x \<in> descendants_of cref (?m43 s cap x) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (?p'43 s cap x) (?m43 s cap x) \<and> usable_untyped_range (?c'43 s cap x) = {} \<or> cref = ?p'43 s cap x)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap x. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; x \<noteq> cref; 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); caps_of_state s x = Some cap; (untyped_range (UntypedCap dev ptr sz idx) \<subseteq> untyped_range cap \<or> untyped_range cap \<subseteq> untyped_range (UntypedCap dev ptr sz idx) \<or> untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}) \<and> (untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}) \<and> (untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subseteq> untyped_range cap \<or> untyped_range cap \<subseteq> untyped_range (UntypedCap dev ptr sz idx) \<or> untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; cref \<in> descendants_of (a, b) (cdt s) \<and> {ptr..ptr + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> usable_untyped_range cap = {}; {ptr..ptr + 2 ^ sz - 1} \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; cref \<in> descendants_of (a, b) (cdt s) \<and> {ptr..ptr + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; {ptr..ptr + 2 ^ sz - 1} \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<subset> untyped_range cap; cref \<in> descendants_of (a, b) (cdt s); {ptr..ptr + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s); (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; cap_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> cap_aligned cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 5. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> ?s115 s cap a b \<turnstile> cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 5. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1}; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; (a, b) \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; cap_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> cap_aligned cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 5. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> ?s131 s cap a b \<turnstile> cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 5. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; (a, b) \<in> descendants_of cref (cdt s); (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> untyped_range cap; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap; cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev ptr sz idx') \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; untyped_range (UntypedCap dev ptr sz idx) \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> untyped_range (UntypedCap dev ptr sz idx) \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> untyped_range (UntypedCap dev ptr sz idx) \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> usable_untyped_range (UntypedCap dev ptr sz idx) = {}; untyped_range (UntypedCap dev ptr sz idx) = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> usable_untyped_range (UntypedCap dev ptr sz idx) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = (a, b); untyped_range (UntypedCap dev ptr sz idx) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of (a, b) (cdt s) \<and> {ptr..ptr + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {}; {ptr..ptr + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range cap = {}; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> cap_aligned cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> ?s152 s cap a b \<turnstile> cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 3. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> untyped_range cap \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 2. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>invs s; S \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx' < 2 ^ sz then {ptr + word_of_nat idx'..ptr + 2 ^ sz - 1} else {}) \<inter> S = {}; descendants_range_in S cref s; is_untyped_cap cap; (a, b) \<noteq> cref; 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); caps_of_state s (a, b) = Some cap; {ptr..ptr + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> untyped_range cap \<inter> S = {} proof (prove)
goal:
No subgoals!