theory Untyped_R

lemma cte_wp_at_caps_no_overlapI':
  "\<lbrakk>invs' s; cte_wp_at' (\<lambda>c. (cteCap c) = capability.UntypedCap
                                            d (ptr && ~~ mask sz) sz idx) cref s;
    idx \<le> unat (ptr && mask sz); sz < word_bits\<rbrakk>
   \<Longrightarrow> caps_no_overlap'' ptr sz s" apply (frule invs_mdb') apply (frule(1) le_mask_le_2p) apply (clarsimp simp:valid_mdb'_def valid_mdb_ctes_def cte_wp_at_ctes_of) apply (case_tac cte) apply simp apply (frule(1) ctes_of_valid_cap'[OF _ invs_valid_objs']) 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) apply simp apply (drule untyped_incD') apply (simp add:isCap_simps)+ 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 (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (elim conjE) apply (drule disjoint_subset2[rotated,
       where B' = "{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}"]) apply clarsimp apply (rule le_plus'[OF word_and_le2]) apply simp apply (erule word_of_nat_le) 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' (\<lambda>c. cteCap c = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; idx \<le> unat (ptr && mask sz); sz < word_bits\<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; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' 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; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; 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 x1 x2. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; 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); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) 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 x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some ctea; isUntypedCap (cteCap ctea); ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea) proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); isUntypedCap x1a; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (5 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); isUntypedCap x1a; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> isUntypedCap (capability.UntypedCap d (ptr && ~~ mask sz) sz idx)
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); isUntypedCap x1a; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> ctes_of s (?p'137 cte x1 x2 ctea x x1a x2a) = Some (CTE (?c'137 cte x1 x2 ctea x x1a x2a) (?n'137 cte x1 x2 ctea x x1a x2a))
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); isUntypedCap x1a; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> isUntypedCap (?c'137 cte x1 x2 ctea x x1a x2a)
 4. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); isUntypedCap x1a; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> untyped_inc' (ctes_of s)
 5. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); isUntypedCap x1a; ctea = CTE x1a x2a; (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subseteq> untypedRange (?c'137 cte x1 x2 ctea x x1a x2a) \<or> untypedRange (?c'137 cte x1 x2 ctea x 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'137 cte x1 x2 ctea x x1a x2a) = {}) \<and> (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<subset> untypedRange (?c'137 cte x1 x2 ctea x x1a x2a) \<longrightarrow> cref \<in> descendants_of' (?p'137 cte x1 x2 ctea x x1a x2a) (ctes_of s) \<and> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<inter> usableUntypedRange (?c'137 cte x1 x2 ctea x x1a x2a) = {}) \<and> (untypedRange (?c'137 cte x1 x2 ctea x x1a x2a) \<subset> untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<longrightarrow> ?p'137 cte x1 x2 ctea x x1a x2a \<in> descendants_of' cref (ctes_of s) \<and> untypedRange (?c'137 cte x1 x2 ctea x x1a x2a) \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}) \<and> (untypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = untypedRange (?c'137 cte x1 x2 ctea x x1a x2a) \<longrightarrow> ?p'137 cte x1 x2 ctea x 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'137 cte x1 x2 ctea x x1a x2a) (ctes_of s) \<and> usableUntypedRange (?c'137 cte x1 x2 ctea x x1a x2a) = {} \<or> cref = ?p'137 cte x1 x2 ctea x x1a x2a)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a \<or> untypedRange x1a \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<or> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}) \<and> ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}) \<and> (untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a \<or> untypedRange x1a \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<or> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (4 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 4. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (4 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<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 x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 4. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (3 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (3 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s); x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1 \<longrightarrow> usableUntypedRange x1a = {} \<or> cref = x; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (3 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (3 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (4 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 4. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (4 subgoals):
 1. \<And>x x2a xa da v0 v1 f. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); 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); valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; ctes_of s x = Some (CTE (capability.UntypedCap da v0 v1 f) x2a); x \<in> descendants_of' cref (ctes_of s); v0 \<le> xa \<longrightarrow> \<not> xa \<le> v0 + 2 ^ v1 - 1; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> v0 + 2 ^ v1 - 1; ptr && ~~ mask sz \<le> v0; v0 + 2 ^ v1 - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr && ~~ mask sz \<le> xa; xa \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; v0 \<le> v0 + 2 ^ v1 - 1; v0 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> ptr
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 4. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (4 subgoals):
 1. \<And>x x2a xa da v0 v1 f. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); 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); valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; ctes_of s x = Some (CTE (capability.UntypedCap da v0 v1 f) x2a); x \<in> descendants_of' cref (ctes_of s); v0 \<le> xa \<longrightarrow> \<not> xa \<le> v0 + 2 ^ v1 - 1; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> v0 + 2 ^ v1 - 1; ptr && ~~ mask sz \<le> v0; v0 + 2 ^ v1 - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr && ~~ mask sz \<le> xa; xa \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; v0 \<le> v0 + 2 ^ v1 - 1; v0 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr - (ptr && ~~ mask sz)
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 4. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (4 subgoals):
 1. \<And>x x2a xa da v0 v1 f. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); 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); valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; ctes_of s x = Some (CTE (capability.UntypedCap da v0 v1 f) x2a); x \<in> descendants_of' cref (ctes_of s); v0 \<le> xa \<longrightarrow> \<not> xa \<le> v0 + 2 ^ v1 - 1; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr \<le> v0 + 2 ^ v1 - 1; ptr && ~~ mask sz \<le> v0; v0 + 2 ^ v1 - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr && ~~ mask sz \<le> xa; xa \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; v0 \<le> v0 + 2 ^ v1 - 1; v0 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr && mask sz
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 4. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (3 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of' cref (ctes_of s); untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 3. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (2 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (2 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (2 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<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 x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untypedRange x1a \<longrightarrow> cref \<in> descendants_of' x (ctes_of s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usableUntypedRange x1a = {}; untypedRange x1a \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> untypedRange x1a \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untypedRange x1a \<longrightarrow> x \<in> descendants_of' cref (ctes_of s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal (2 subgoals):
 1. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cte x1 x2 ctea x x1a x2a. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; valid_dlist (ctes_of s); x1 = 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); cte = CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2; valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s; untypedRange x1a \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s x = Some (CTE x1a x2a); \<exists>d v0 v1 f. x1a = capability.UntypedCap d v0 v1 f; ctea = CTE x1a x2a; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untypedRange x1a = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange x1a proof (prove)
goal:
No subgoals!