theory Untyped_AI

lemma descendants_range_caps_no_overlapI:
  "\<lbrakk>invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s;
  descendants_range_in {ptr .. (ptr && ~~ mask sz) +2^sz - 1} cref s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s" apply (frule invs_mdb) apply (clarsimp simp: valid_mdb_def cte_wp_at_caps_of_state) apply (unfold caps_no_overlap_def) apply (intro ballI impI) apply (erule ranE) apply (subgoal_tac "is_untyped_cap cap") prefer 2 apply (rule untyped_range_is_untyped_cap) apply blast apply (drule untyped_incD) apply simp+ apply (elim conjE) apply (erule subset_splitE) apply (erule subset_trans[OF _ psubset_imp_subset,rotated]) apply (clarsimp simp: word_and_le2) apply simp apply (elim conjE) apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (drule(2) descendants_range_inD) apply simp apply simp apply (erule subset_trans[OF _  equalityD1,rotated]) apply (clarsimp simp: word_and_le2) apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (drule disjoint_subset[rotated,
       where A' = "{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}"]) apply (clarsimp simp: word_and_le2 Int_ac)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; valid_mdb s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; 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); cap \<in> ran (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 2. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> untyped_range cap \<noteq> {}
 2. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (5 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> caps_of_state s (?p'29 cap x) = Some (?c'29 cap x)
 3. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> is_untyped_cap (?c'29 cap x)
 4. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> untyped_inc (?m29 cap x) (caps_of_state s)
 5. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<subseteq> untyped_range (?c'29 cap x) \<or> untyped_range (?c'29 cap x) \<subseteq> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<or> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> untyped_range (?c'29 cap x) = {}) \<and> (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<subset> untyped_range (?c'29 cap x) \<longrightarrow> cref \<in> descendants_of (?p'29 cap x) (?m29 cap x) \<and> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> usable_untyped_range (?c'29 cap x) = {}) \<and> (untyped_range (?c'29 cap x) \<subset> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<longrightarrow> ?p'29 cap x \<in> descendants_of cref (?m29 cap x) \<and> untyped_range (?c'29 cap x) \<inter> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {}) \<and> (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = untyped_range (?c'29 cap x) \<longrightarrow> ?p'29 cap x \<in> descendants_of cref (?m29 cap x) \<and> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of (?p'29 cap x) (?m29 cap x) \<and> usable_untyped_range (?c'29 cap x) = {} \<or> cref = ?p'29 cap x)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap \<or> untyped_range cap \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<or> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}) \<and> ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}) \<and> ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap \<or> untyped_range cap \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<or> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 4. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 4. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s); x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s); {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; cap_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cap x. \<lbrakk>invs s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal:
No subgoals!