theory Untyped_R

lemma updateFreeIndex_updateCap_caps_overlap_reserved:
  "\<lbrace>\<lambda>s. valid_mdb' s \<and> valid_objs' s \<and> S \<subseteq> untypedRange cap \<and>
        usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {} \<and>
        isUntypedCap cap \<and> descendants_range_in' S src (ctes_of s) \<and>
        cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace>
   updateCap src (capFreeIndex_update (\<lambda>_. index) cap)
   \<lbrace>\<lambda>r s. caps_overlap_reserved' S s\<rbrace>" apply (clarsimp simp:caps_overlap_reserved'_def) apply (wp updateCap_ctes_of_wp) apply (clarsimp simp:modify_map_def cte_wp_at_ctes_of) apply (erule ranE) apply (clarsimp split:if_split_asm simp:valid_mdb'_def valid_mdb_ctes_def) apply (case_tac cte) apply (case_tac ctea) apply simp apply (drule untyped_incD') apply (simp+)[4] apply clarify apply (erule subset_splitE) apply (simp del:usable_untyped_range.simps) apply (thin_tac "P \<longrightarrow> Q" for P Q)+ apply (elim conjE) apply blast apply (simp) apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (elim conjE) apply (drule(2) descendants_range_inD') apply simp apply (rule disjoint_subset[OF usableRange_subseteq]) apply (rule valid_capAligned) apply (erule(1) ctes_of_valid_cap') apply (simp add:untypedCapRange)+ apply (elim disjE) apply clarsimp apply (drule(2) descendants_range_inD') apply simp apply (rule disjoint_subset[OF usableRange_subseteq]) apply (rule valid_capAligned) apply (erule(1) ctes_of_valid_cap') apply (simp add:untypedCapRange)+ apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (rule disjoint_subset[OF usableRange_subseteq]) apply (rule valid_capAligned) apply (erule(1) ctes_of_valid_cap') apply simp+ apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb' s \<and> valid_objs' s \<and> S \<subseteq> untypedRange cap \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {} \<and> isUntypedCap cap \<and> descendants_range_in' S src (ctes_of s) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r. caps_overlap_reserved' S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb' s \<and> valid_objs' s \<and> S \<subseteq> untypedRange cap \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {} \<and> isUntypedCap cap \<and> descendants_range_in' S src (ctes_of s) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r s. \<forall>cte\<in>ran (ctes_of s). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_mdb' s \<and> valid_objs' s \<and> S \<subseteq> untypedRange cap \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {} \<and> isUntypedCap cap \<and> descendants_range_in' S src (ctes_of s) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> \<forall>cte\<in>ran (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>cte \<in> ran (\<lambda>a. if a = src then map_option (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea))) (ctes_of s src) else ctes_of s a); valid_mdb' s; valid_objs' s; S \<subseteq> untypedRange (cteCap ctea); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> S = {}; isUntypedCap (cteCap ctea); descendants_range_in' S src (ctes_of s); ctes_of s src = Some ctea; cap = cteCap ctea; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x. \<lbrakk>valid_mdb' s; valid_objs' s; S \<subseteq> untypedRange (cteCap ctea); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> S = {}; isUntypedCap (cteCap ctea); descendants_range_in' S src (ctes_of s); ctes_of s src = Some ctea; cap = cteCap ctea; isUntypedCap (cteCap cte); (if x = src then map_option (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea))) (ctes_of s src) else ctes_of s x) = Some cte\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange (cteCap ctea); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> S = {}; isUntypedCap (cteCap ctea); descendants_range_in' S src (ctes_of s); ctes_of s src = Some ctea; cap = cteCap ctea; isUntypedCap (cteCap cte); x \<noteq> src; 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); ctes_of s x = Some cte\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange (cteCap ctea); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> S = {}; isUntypedCap (cteCap ctea); descendants_range_in' S src (ctes_of s); ctes_of s src = Some ctea; cap = cteCap ctea; isUntypedCap (cteCap cte); x \<noteq> src; 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); ctes_of s x = Some cte; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange (cteCap ctea); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> S = {}; isUntypedCap (cteCap ctea); descendants_range_in' S src (ctes_of s); ctes_of s src = Some ctea; cap = cteCap ctea; isUntypedCap (cteCap cte); x \<noteq> src; 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); ctes_of s x = Some cte; cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1a; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) x1a) \<inter> S = {}; isUntypedCap x1a; descendants_range_in' S src (ctes_of s); ctes_of s src = Some (CTE x1a x2a); cap = x1a; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1a; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) x1a) \<inter> S = {}; isUntypedCap x1a; descendants_range_in' S src (ctes_of s); cap = x1a; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> isUntypedCap x1a
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1a; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) x1a) \<inter> S = {}; isUntypedCap x1a; descendants_range_in' S src (ctes_of s); cap = x1a; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> ctes_of s (?p'64 s cte ctea x x1 x2 x1a x2a) = Some (CTE (?c'64 s cte ctea x x1 x2 x1a x2a) (?n'64 s cte ctea x x1 x2 x1a x2a))
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1a; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) x1a) \<inter> S = {}; isUntypedCap x1a; descendants_range_in' S src (ctes_of s); cap = x1a; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> isUntypedCap (?c'64 s cte ctea x x1 x2 x1a x2a)
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1a; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) x1a) \<inter> S = {}; isUntypedCap x1a; descendants_range_in' S src (ctes_of s); cap = x1a; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); cte = CTE x1 x2; ctea = CTE x1a x2a\<rbrakk> \<Longrightarrow> untyped_inc' (ctes_of s)
 5. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1a; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) x1a) \<inter> S = {}; isUntypedCap x1a; descendants_range_in' S src (ctes_of s); cap = x1a; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); cte = CTE x1 x2; ctea = CTE x1a x2a; (untypedRange x1a \<subseteq> untypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) \<or> untypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) \<subseteq> untypedRange x1a \<or> untypedRange x1a \<inter> untypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) = {}) \<and> (untypedRange x1a \<subset> untypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) \<longrightarrow> src \<in> descendants_of' (?p'64 s cte ctea x x1 x2 x1a x2a) (ctes_of s) \<and> untypedRange x1a \<inter> usableUntypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) = {}) \<and> (untypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) \<subset> untypedRange x1a \<longrightarrow> ?p'64 s cte ctea x x1 x2 x1a x2a \<in> descendants_of' src (ctes_of s) \<and> untypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) \<inter> usableUntypedRange x1a = {}) \<and> (untypedRange x1a = untypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) \<longrightarrow> ?p'64 s cte ctea x x1 x2 x1a x2a \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> src \<in> descendants_of' (?p'64 s cte ctea x x1 x2 x1a x2a) (ctes_of s) \<and> usableUntypedRange (?c'64 s cte ctea x x1 x2 x1a x2a) = {} \<or> src = ?p'64 s cte ctea x x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1a; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) x1a) \<inter> S = {}; isUntypedCap x1a; descendants_range_in' S src (ctes_of s); cap = x1a; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); cte = CTE x1 x2; ctea = CTE x1a x2a; (untypedRange x1a \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange x1a \<or> untypedRange x1a \<inter> untypedRange x1 = {}) \<and> (untypedRange x1a \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange x1a \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange x1a \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange x1a = {}) \<and> (untypedRange x1a = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x)\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange x1 = {}; untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<subset> untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange x1 \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> usableUntypedRange cap = {} \<or> usableUntypedRange x1 = {}; untypedRange cap \<subset> untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange x1 \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange cap \<subset> untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange x1 \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1; src \<in> descendants_of' x (ctes_of s); untypedRange cap \<inter> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange x1 \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange x1 \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> usableUntypedRange cap = {} \<or> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange x1 \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange (cteCap (CTE x1 x2)) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> capAligned x1
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 3. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {}
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 5. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> valid_cap' x1 (?s165 s x x1 x2)
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 3. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {}
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 5. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange x1 \<subset> untypedRange cap; x \<in> descendants_of' src (ctes_of s); untypedRange x1 \<inter> usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}; untypedRange cap = untypedRange x1\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange (cteCap (CTE x1 x2)) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 3. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> capAligned x1
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 3. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {}
 4. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 5. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (5 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> valid_cap' x1 (?s182 s x x1 x2)
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 3. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {}
 4. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 5. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; x \<in> descendants_of' src (ctes_of s); usableUntypedRange cap = {}; capRange x1 \<inter> S = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {}
 3. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange x1; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap = untypedRange x1; src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {}
 4. \<And>s cte ctea x x1 x2 x1a x2a. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> src = x; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<subset> untypedRange x1 \<longrightarrow> src \<in> descendants_of' x (ctes_of s) \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}; untypedRange x1 \<subset> untypedRange cap \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange x1 \<longrightarrow> x \<in> descendants_of' src (ctes_of s) \<and> usableUntypedRange cap = {} \<or> src \<in> descendants_of' x (ctes_of s) \<and> usableUntypedRange x1 = {}; untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> usableUntypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> capAligned x1
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 3. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> valid_cap' x1 (?s203 s x x1 x2)
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 3. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> isUntypedCap x1
 2. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x x1 x2. \<lbrakk>valid_objs' s; S \<subseteq> untypedRange cap; usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {}; isUntypedCap cap; descendants_range_in' S src (ctes_of s); isUntypedCap x1; x \<noteq> src; 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); ctes_of s x = Some (CTE x1 x2); untypedRange cap \<inter> untypedRange x1 = {}\<rbrakk> \<Longrightarrow> untypedRange x1 \<inter> S = {} proof (prove)
goal:
No subgoals!