theory Untyped_R

lemma descendants_range_caps_no_overlapI':
  "\<lbrakk>invs' s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap
                                          d (ptr && ~~ mask sz) sz idx) cref s;
    descendants_range_in' {ptr .. (ptr && ~~ mask sz) +2^sz - 1} cref
                          (ctes_of s)\<rbrakk>
   \<Longrightarrow> caps_no_overlap'' ptr sz s" apply (frule invs_mdb') apply (clarsimp simp:valid_mdb'_def valid_mdb_ctes_def cte_wp_at_ctes_of
         simp del:usableUntypedRange.simps untypedRange.simps) apply (unfold caps_no_overlap''_def) apply (intro ballI impI) apply (erule ranE) apply (subgoal_tac "isUntypedCap (cteCap ctea)") prefer 2 apply (rule untypedRange_not_emptyD) apply blast apply (case_tac ctea,case_tac cte) apply simp apply (drule untyped_incD') apply ((simp add:isCap_simps del:usableUntypedRange.simps untypedRange.simps)+)[4] apply (elim conjE 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 add:untypedCapRange)+ 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' (\<lambda>c. cteCap c = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s)\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_mdb' s\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> \<forall>cte\<in>ran (ctes_of s). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte ctea. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctea \<in> ran (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea) proof (prove)
goal (1 subgoal):
 1. \<And>cte ctea x. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea) proof (prove)
goal (2 subgoals):
 1. \<And>cte ctea x. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea; isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea)
 2. \<And>cte ctea x. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ctea) proof (prove)
goal (2 subgoals):
 1. \<And>cte ctea x. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ctea)
 2. \<And>cte ctea x. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea; isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea) proof (prove)
goal (2 subgoals):
 1. \<And>cte ctea x. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea\<rbrakk> \<Longrightarrow> untypedRange (cteCap ctea) \<noteq> {}
 2. \<And>cte ctea x. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea; isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea) proof (prove)
goal (1 subgoal):
 1. \<And>cte ctea x. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea; isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea) proof (prove)
goal (1 subgoal):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea; isUntypedCap (cteCap ctea); ctea = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea) proof (prove)
goal (1 subgoal):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (5 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a\<rbrakk> \<Longrightarrow> isUntypedCap (capability.UntypedCap d (ptr && ~~ mask sz) sz idx)
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a\<rbrakk> \<Longrightarrow> ctes_of s (?p'37 cte ctea x x1 x2 x1a x2a) = Some (CTE (?c'37 cte ctea x x1 x2 x1a x2a) (?n'37 cte ctea x x1 x2 x1a x2a))
 3. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a\<rbrakk> \<Longrightarrow> isUntypedCap (?c'37 cte ctea x x1 x2 x1a x2a)
 4. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a\<rbrakk> \<Longrightarrow> untyped_inc' (ctes_of s)
 5. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subseteq> untypedRange (?c'37 cte ctea x x1 x2 x1a x2a) \<or> untypedRange (?c'37 cte ctea x x1 x2 x1a x2a) \<subseteq> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<or> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange (?c'37 cte ctea x x1 x2 x1a x2a) = {}) \<and> (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange (?c'37 cte ctea x x1 x2 x1a x2a) \<longrightarrow> cref \<in> descendants_of' (?p'37 cte ctea x x1 x2 x1a x2a) (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange (?c'37 cte ctea x x1 x2 x1a x2a) = {}) \<and> (untypedRange (?c'37 cte ctea x x1 x2 x1a x2a) \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> ?p'37 cte ctea x x1 x2 x1a x2a \<in> descendants_of' cref (ctes_of s) \<and> untypedRange (?c'37 cte ctea x x1 x2 x1a x2a) \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}) \<and> (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange (?c'37 cte ctea x x1 x2 x1a x2a) \<longrightarrow> ?p'37 cte ctea x x1 x2 x1a x2a \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' (?p'37 cte ctea x x1 x2 x1a x2a) (ctes_of s) \<and> usableUntypedRange (?c'37 cte ctea x x1 x2 x1a x2a) = {} \<or> cref = ?p'37 cte ctea x x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (1 subgoal):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<or> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}) \<and> (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}) \<and> (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (4 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 3. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 4. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (4 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx)
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 3. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 4. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (3 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 3. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (3 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s); x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<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} = untypedRange x1 \<longrightarrow> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> usableUntypedRange x1 = {} \<or> cref = x; untypedRange x1 \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 3. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (3 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s); {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1 \<longrightarrow> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {} \<or> usableUntypedRange x1 = {} \<or> cref = x; untypedRange x1 \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1 \<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> untypedRange x1
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 3. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (3 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange x1 \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1 \<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> untypedRange x1
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 3. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (3 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange x1 \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1 \<inter> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) = {}; capRange (cteCap (CTE x1 x2)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 3. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (2 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; x \<in> descendants_of' cref (ctes_of 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 (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (2 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; x \<in> descendants_of' cref (ctes_of 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 (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (1 subgoal):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange x1 \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange x1 \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> cref = x; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (1 subgoal):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal (2 subgoals):
 1. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx)
 2. \<And>cte ctea x x1 x2 x1a x2a. \<lbrakk>invs' s; descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s); valid_dlist (ctes_of s); x1a = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); untypedRange x1 \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1 x2); isUntypedCap x1; ctea = CTE x1 x2; cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2a; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1 proof (prove)
goal:
No subgoals!