theory Untyped_R

lemma untypedCap_descendants_range':
  "\<lbrakk>valid_pspace' s; (ctes_of s) p = Some cte;
    isUntypedCap (cteCap cte);valid_mdb' s;
    q \<in> descendants_of' p (ctes_of s)\<rbrakk>
   \<Longrightarrow> cte_wp_at' (\<lambda>c. (capRange (cteCap c) \<inter>
                        usableUntypedRange (cteCap cte) = {})) q s" apply (clarsimp simp: valid_pspace'_def) apply (frule(1) descendants_of_cte_at') apply (clarsimp simp:cte_wp_at_ctes_of) apply (clarsimp simp:valid_mdb'_def) apply (frule valid_mdb_no_loops) apply (case_tac "isUntypedCap (cteCap ctea)") apply (case_tac ctea) apply (rename_tac cap node) apply (case_tac cte) apply (rename_tac cap' node') apply clarsimp apply (frule(1) valid_capAligned[OF ctes_of_valid_cap']) apply (frule_tac c = cap in valid_capAligned[OF ctes_of_valid_cap']) apply (simp add:untypedCapRange)+ apply (frule_tac c = cap' in aligned_untypedRange_non_empty) apply simp apply (frule_tac c = cap in aligned_untypedRange_non_empty) apply simp apply (clarsimp simp:valid_mdb'_def valid_mdb_ctes_def) apply (drule untyped_incD') apply simp+ apply clarify apply (erule subset_splitE) apply simp apply (thin_tac "P \<longrightarrow> Q" for P Q)+ apply (elim conjE) apply (simp add:descendants_of'_def) apply (drule(1) subtree_trans) apply (simp add:no_loops_no_subtree) apply simp apply (clarsimp simp:descendants_of'_def | erule disjE)+ apply (drule(1) subtree_trans) apply (simp add:no_loops_no_subtree)+ apply (thin_tac "P \<longrightarrow> Q" for P Q)+ apply (erule(1) disjoint_subset2[OF usableRange_subseteq]) apply (simp add:Int_ac) apply (case_tac ctea) apply (rename_tac cap node) apply (case_tac cte) apply clarsimp apply (drule(1) ctes_of_valid_cap')+ apply (frule_tac cap = cap in ctes_of_ko) apply (elim disjE) apply clarsimp+ apply (thin_tac "s \<turnstile>' cap") apply (clarsimp simp: valid_cap'_def isCap_simps valid_untyped'_def
                  simp del: usableUntypedRange.simps untypedRange.simps) apply (thin_tac "\<forall>x y z. P x y z" for P) apply (rule ccontr) apply (clarsimp dest!: int_not_emptyD
                  simp del: usableUntypedRange.simps untypedRange.simps) apply (drule(1) bspec) apply (clarsimp simp: ko_wp_at'_def simp del: usableUntypedRange.simps untypedRange.simps) apply (drule_tac x = optr in spec) apply (clarsimp simp: ko_wp_at'_def simp del: usableUntypedRange.simps untypedRange.simps) apply (frule(1) pspace_alignedD') apply (frule(1) pspace_distinctD') apply (erule(1) impE) apply (clarsimp simp del: usableUntypedRange.simps untypedRange.simps) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb' s; q \<in> descendants_of' p (ctes_of s)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> usableUntypedRange (cteCap cte) = {}) q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb' s; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> usableUntypedRange (cteCap cte) = {}) q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb' s; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; cte_wp_at' (\<lambda>_. True) q s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> usableUntypedRange (cteCap cte) = {}) q s proof (prove)
goal (1 subgoal):
 1. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb' s; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ctea x1 x2. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); isUntypedCap (cteCap ctea); ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ctea cap node. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); isUntypedCap (cteCap ctea); ctea = CTE cap node\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ctea cap node x1 x2. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); isUntypedCap (cteCap ctea); ctea = CTE cap node; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ctea cap node cap' node'. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); isUntypedCap (cteCap ctea); ctea = CTE cap node; cte = CTE cap' node'\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (3 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (3 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap\<rbrakk> \<Longrightarrow> isUntypedCap cap'
 2. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (3 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> isUntypedCap cap
 2. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>ctes_of s p = Some (CTE cap' node'); isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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)\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (6 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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)\<rbrakk> \<Longrightarrow> isUntypedCap cap'
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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)\<rbrakk> \<Longrightarrow> ctes_of s (?p'41 cap node cap' node') = Some (CTE (?c'41 cap node cap' node') (?n'41 cap node cap' node'))
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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)\<rbrakk> \<Longrightarrow> isUntypedCap (?c'41 cap node cap' node')
 4. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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)\<rbrakk> \<Longrightarrow> untyped_inc' (ctes_of s)
 5. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); (untypedRange cap' \<subseteq> untypedRange (?c'41 cap node cap' node') \<or> untypedRange (?c'41 cap node cap' node') \<subseteq> untypedRange cap' \<or> untypedRange cap' \<inter> untypedRange (?c'41 cap node cap' node') = {}) \<and> (untypedRange cap' \<subset> untypedRange (?c'41 cap node cap' node') \<longrightarrow> p \<in> descendants_of' (?p'41 cap node cap' node') (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange (?c'41 cap node cap' node') = {}) \<and> (untypedRange (?c'41 cap node cap' node') \<subset> untypedRange cap' \<longrightarrow> ?p'41 cap node cap' node' \<in> descendants_of' p (ctes_of s) \<and> untypedRange (?c'41 cap node cap' node') \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' = untypedRange (?c'41 cap node cap' node') \<longrightarrow> ?p'41 cap node cap' node' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' (?p'41 cap node cap' node') (ctes_of s) \<and> usableUntypedRange (?c'41 cap node cap' node') = {} \<or> p = ?p'41 cap node cap' node')\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 6. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); (untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<inter> untypedRange cap = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q)\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<inter> untypedRange cap = {}; untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (5 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap \<subset> untypedRange cap'\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 5. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (5 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap \<subset> untypedRange cap'\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 5. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (5 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap \<subset> untypedRange cap'\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 5. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (5 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<subset> untypedRange cap; p \<in> descendants_of' q (ctes_of s); untypedRange cap' \<inter> usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap \<subset> untypedRange cap'\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 5. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (5 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; ctes_of s \<turnstile> p \<rightarrow> q; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<subset> untypedRange cap; ctes_of s \<turnstile> q \<rightarrow> p; untypedRange cap' \<inter> usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap \<subset> untypedRange cap'\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 5. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (5 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<subset> untypedRange cap; ctes_of s \<turnstile> q \<rightarrow> p; untypedRange cap' \<inter> usableUntypedRange cap = {}; ctes_of s \<turnstile> p \<rightarrow> p\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap \<subset> untypedRange cap'\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 5. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (4 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap \<subset> untypedRange cap'\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (3 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (4 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; ctes_of s \<turnstile> p \<rightarrow> q; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap \<noteq> {}; 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); untypedRange cap' = untypedRange cap; ctes_of s \<turnstile> q \<rightarrow> p; usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; ctes_of s \<turnstile> p \<rightarrow> q; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap \<noteq> {}; 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); untypedRange cap' = untypedRange cap; p = q\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (4 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap \<noteq> {}; 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); untypedRange cap' = untypedRange cap; ctes_of s \<turnstile> q \<rightarrow> p; usableUntypedRange cap = {}; ctes_of s \<turnstile> p \<rightarrow> p\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; ctes_of s \<turnstile> p \<rightarrow> q; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap \<noteq> {}; 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); untypedRange cap' = untypedRange cap; p = q\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 3. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 4. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p \<in> descendants_of' q (ctes_of s) \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap' = untypedRange cap \<longrightarrow> usableUntypedRange cap' = {} \<or> p \<in> descendants_of' q (ctes_of s) \<and> usableUntypedRange cap = {} \<or> p = q; \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> usableUntypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node cap' node'. \<lbrakk>isUntypedCap cap'; q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); isUntypedCap cap; cte = CTE cap' node'; capAligned cap; untypedRange cap' \<noteq> {}; untypedRange cap \<noteq> {}; 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); \<not> untypedRange cap \<subset> untypedRange cap'; untypedRange cap' \<inter> untypedRange cap = {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> untypedRange cap' = {}
 2. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ctea. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ctea x1 x2. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea); ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ctea cap node. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea); ctea = CTE cap node\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ctea cap node x1 x2. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some ctea; no_loops (ctes_of s); \<not> isUntypedCap (cteCap ctea); ctea = CTE cap node; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> usableUntypedRange (cteCap cte) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap node x1 x2. \<lbrakk>ctes_of s p = Some (CTE x1 x2); isUntypedCap x1; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; ctes_of s q = Some (CTE cap node); no_loops (ctes_of s); \<not> isUntypedCap cap; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange x1 = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap node x1 x2. \<lbrakk>isUntypedCap x1; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); \<not> isUntypedCap cap; cte = CTE x1 x2; valid_cap' x1 s; valid_cap' cap s\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange x1 = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap node x1 x2. \<lbrakk>isUntypedCap x1; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); \<not> isUntypedCap cap; cte = CTE x1 x2; valid_cap' x1 s; valid_cap' cap s; isUntypedCap cap \<or> (\<forall>ptr\<in>capRange cap. \<exists>optr ko. ksPSpace s optr = Some ko \<and> ptr \<in> obj_range' optr ko)\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange x1 = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap node x1 x2. \<lbrakk>isUntypedCap x1; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); \<not> isUntypedCap cap; cte = CTE x1 x2; valid_cap' x1 s; valid_cap' cap s; isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange x1 = {}
 2. \<And>cap node x1 x2. \<lbrakk>isUntypedCap x1; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); \<not> isUntypedCap cap; cte = CTE x1 x2; valid_cap' x1 s; valid_cap' cap s; \<forall>ptr\<in>capRange cap. \<exists>optr ko. ksPSpace s optr = Some ko \<and> ptr \<in> obj_range' optr ko\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange x1 = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap x1 x2. \<lbrakk>isUntypedCap x1; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); \<not> isUntypedCap cap; cte = CTE x1 x2; valid_cap' x1 s; valid_cap' cap s; \<forall>ptr\<in>capRange cap. \<exists>optr ko. ksPSpace s optr = Some ko \<and> ptr \<in> obj_range' optr ko\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange x1 = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap x1 x2. \<lbrakk>isUntypedCap x1; valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); \<not> isUntypedCap cap; cte = CTE x1 x2; valid_cap' x1 s; \<forall>ptr\<in>capRange cap. \<exists>optr ko. ksPSpace s optr = Some ko \<and> ptr \<in> obj_range' optr ko\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange x1 = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); \<forall>d v0 v1 f. cap \<noteq> capability.UntypedCap d v0 v1 f; cte = CTE (capability.UntypedCap d v0 v1 f) x2; \<forall>ptr\<in>capRange cap. \<exists>optr ko. ksPSpace s optr = Some ko \<and> ptr \<in> obj_range' optr ko; capAligned (capability.UntypedCap d v0 v1 f); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {}) ptr' s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; \<forall>ptr\<in>capRange cap. \<exists>optr ko. ksPSpace s optr = Some ko \<and> ptr \<in> obj_range' optr ko; capAligned (capability.UntypedCap d v0 v1 f); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {}) ptr' s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> capRange cap \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; \<forall>ptr\<in>capRange cap. \<exists>optr ko. ksPSpace s optr = Some ko \<and> ptr \<in> obj_range' optr ko; capAligned (capability.UntypedCap d v0 v1 f); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {}) ptr' s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; capRange cap \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; \<forall>ptr\<in>capRange cap. \<exists>optr ko. ksPSpace s optr = Some ko \<and> ptr \<in> obj_range' optr ko; capAligned (capability.UntypedCap d v0 v1 f); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {}) ptr' s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; capAligned (capability.UntypedCap d v0 v1 f); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {}) ptr' s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f); \<exists>optr ko. ksPSpace s optr = Some ko \<and> x \<in> obj_range' optr ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x optr ko. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; capAligned (capability.UntypedCap d v0 v1 f); \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f); ksPSpace s optr = Some ko; x \<in> obj_range' optr ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x optr ko. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; capAligned (capability.UntypedCap d v0 v1 f); v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f); ksPSpace s optr = Some ko; x \<in> obj_range' optr ko; \<forall>ko. is_aligned optr (objBitsKO ko) \<longrightarrow> ksPSpace s optr = Some ko \<longrightarrow> \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' optr ko \<and> obj_range' optr ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {} \<or> \<not> ps_clear optr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x optr ko. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; capAligned (capability.UntypedCap d v0 v1 f); v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f); ksPSpace s optr = Some ko; x \<in> obj_range' optr ko; is_aligned optr (objBitsKO ko) \<longrightarrow> \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' optr ko \<and> obj_range' optr ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {} \<or> \<not> ps_clear optr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x optr ko. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; capAligned (capability.UntypedCap d v0 v1 f); v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f); ksPSpace s optr = Some ko; x \<in> obj_range' optr ko; is_aligned optr (objBitsKO ko) \<longrightarrow> \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' optr ko \<and> obj_range' optr ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {} \<or> \<not> ps_clear optr (objBitsKO ko) s; is_aligned optr (objBitsKO ko)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x optr ko. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; capAligned (capability.UntypedCap d v0 v1 f); v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f); ksPSpace s optr = Some ko; x \<in> obj_range' optr ko; is_aligned optr (objBitsKO ko) \<longrightarrow> \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' optr ko \<and> obj_range' optr ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {} \<or> \<not> ps_clear optr (objBitsKO ko) s; is_aligned optr (objBitsKO ko); ps_clear optr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x optr ko. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; capAligned (capability.UntypedCap d v0 v1 f); v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f); ksPSpace s optr = Some ko; x \<in> obj_range' optr ko; is_aligned optr (objBitsKO ko); ps_clear optr (objBitsKO ko) s; \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' optr ko \<and> obj_range' optr ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {} \<or> \<not> ps_clear optr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x2 d v0 v1 f x optr ko. \<lbrakk>valid_mdb_ctes (ctes_of s); q \<in> descendants_of' p (ctes_of s); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; no_loops (ctes_of s); cte = CTE (capability.UntypedCap d v0 v1 f) x2; capAligned (capability.UntypedCap d v0 v1 f); v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; x \<in> capRange cap; x \<in> usableUntypedRange (capability.UntypedCap d v0 v1 f); ksPSpace s optr = Some ko; x \<in> obj_range' optr ko; is_aligned optr (objBitsKO ko); ps_clear optr (objBitsKO ko) s; \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' optr ko; obj_range' optr ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!