theory Untyped_R

lemma caps_contained_n' [simp]: "caps_contained' n'" using caps_contained untyped_mdb untyped_inc apply (clarsimp simp: caps_contained'_def) apply (drule n'_cap)+ apply (clarsimp split: if_split_asm) apply (drule capRange_untyped) apply simp apply (frule capRange_untyped) apply (frule untypedRange_c') apply (erule_tac x=parent in allE) apply (erule_tac x=p' in allE) apply (simp add: parent) apply (erule impE, blast) apply (simp add: untyped_mdb'_def) apply (erule_tac x=parent in allE) apply (erule_tac x=p' in allE) apply (simp add: parent is_untyped descendants_of'_def) apply (erule impE) apply (thin_tac "m site = t" for t) apply (drule valid_capI') apply (frule valid_capAligned) apply blast apply (drule (1) rangeD) apply (frule capRange_untyped) apply (drule untypedCapRange) apply simp apply (thin_tac "All P" for P) apply (insert capRange_c')[1] apply (simp add: untypedCapRange is_untyped) apply (subgoal_tac "untypedRange parent_cap \<inter> untypedRange c \<noteq> {}") prefer 2 apply blast apply (frule untyped_incD'[OF _ capRange_untyped _ is_untyped]) apply (case_tac c) apply simp_all apply (simp add:isCap_simps) apply (rule parent) apply clarsimp apply (case_tac "untypedRange c = untypedRange parent_cap") apply blast apply simp apply (elim disjE) apply (drule_tac A = "untypedRange c" in psubsetI) apply simp+ apply (thin_tac "P\<longrightarrow>Q" for P Q) apply (elim conjE) apply (simp add:descendants_of'_def) apply (drule(1) rangeD) apply (frule capRange_untyped) apply (simp add:untypedCapRange Int_ac) apply blast apply (simp add:descendants_of'_def) apply blast apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_contained' n' proof (prove)
using this:
caps_contained' m
untyped_mdb' m
untyped_inc' m

goal (1 subgoal):
 1. caps_contained' n' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'a x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; n' p = Some (CTE c n); n' p' = Some (CTE c' n'a); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c'a n' x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; if p = site then c = c' \<and> m p = Some (CTE capability.NullCap site_node) else \<exists>node'. m p = Some (CTE c node'); if p' = site then c'a = c' \<and> m p' = Some (CTE capability.NullCap site_node) else \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'; m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p' c'a x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 3. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; x \<in> capRange c'; m site = Some (CTE capability.NullCap site_node); isUntypedCap c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p' c'a x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 3. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; \<forall>p' c. (\<exists>n. m parent = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; \<forall>c. (\<exists>n. m parent = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<inter> untypedRange parent_cap \<noteq> {} \<longrightarrow> capRange c'a \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; \<forall>p' c. (\<exists>n. m parent = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' parent m)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; \<forall>c. (\<exists>n. m parent = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' parent m)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; capRange c'a \<inter> untypedRange parent_cap \<noteq> {} \<longrightarrow> m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> capRange c'a \<inter> untypedRange parent_cap \<noteq> {}
 2. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 3. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> capRange c'a \<inter> untypedRange parent_cap \<noteq> {}
 2. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 3. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; p' \<noteq> site; isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; valid_cap' c'a s\<rbrakk> \<Longrightarrow> capRange c'a \<inter> untypedRange parent_cap \<noteq> {}
 2. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 3. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; p' \<noteq> site; isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; valid_cap' c'a s; capAligned c'a\<rbrakk> \<Longrightarrow> capRange c'a \<inter> untypedRange parent_cap \<noteq> {}
 2. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 3. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; capRange c'a \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); isUntypedCap c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; capRange c'a \<inter> capRange c' = {}; isUntypedCap c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'. \<lbrakk>untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<subseteq> untypedRange parent_cap; capRange c'a \<inter> capRange c' = {}; isUntypedCap c'; capRange c' = untypedRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> capRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> untypedRange parent_cap \<inter> untypedRange c \<noteq> {}
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> untypedRange parent_cap \<inter> untypedRange c \<noteq> {}
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (5 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> m (?p'162 p c x node') = Some (CTE parent_cap (?n'162 p c x node'))
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> untyped_inc' m
 4. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; (untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}) \<and> (untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' (?p'162 p c x node') m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}) \<and> (untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> ?p'162 p c x node' \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange parent_cap \<longrightarrow> ?p'162 p c x node' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' (?p'162 p c x node') m \<and> usableUntypedRange parent_cap = {} \<or> p = ?p'162 p c x node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 5. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (16 subgoals):
 1. \<And>p c x node' x1. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.NullCap\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 3. \<And>p c x node' x31 x32 x33 x34. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 4. \<And>p c x node' x4. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 5. \<And>p c x node' x51 x52 x53 x54 x55 x56. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 6. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.DomainCap\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 7. \<And>p c x node' x71 x72 x73. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 8. \<And>p c x node' x8. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 9. \<And>p c x node' x91 x92 x93. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
 10. \<And>p c x node' x101 x102 x103 x104. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> capRange (?cap'162 p c x node') \<inter> untypedRange c \<noteq> {}
A total of 16 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> m (?p'162 p c x node') = Some (CTE parent_cap (?n'162 p c x node'))
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; (untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}) \<and> (untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' (?p'162 p c x node') m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}) \<and> (untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> ?p'162 p c x node' \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange parent_cap \<longrightarrow> ?p'162 p c x node' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' (?p'162 p c x node') m \<and> usableUntypedRange parent_cap = {} \<or> p = ?p'162 p c x node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> m (?p'162 p c x node') = Some (CTE parent_cap (?n'162 p c x node'))
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; (untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}) \<and> (untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' (?p'162 p c x node') m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}) \<and> (untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> ?p'162 p c x node' \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange parent_cap \<longrightarrow> ?p'162 p c x node' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' (?p'162 p c x node') m \<and> usableUntypedRange parent_cap = {} \<or> p = ?p'162 p c x node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; (untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}) \<and> (untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}) \<and> (untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange parent_cap \<longrightarrow> parent \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' parent m \<and> usableUntypedRange parent_cap = {} \<or> p = parent)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c = untypedRange parent_cap \<longrightarrow> parent \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' parent m \<and> usableUntypedRange parent_cap = {} \<or> p = parent\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c = untypedRange parent_cap \<longrightarrow> parent \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' parent m \<and> usableUntypedRange parent_cap = {} \<or> p = parent; untypedRange c = untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c = untypedRange parent_cap \<longrightarrow> parent \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' parent m \<and> usableUntypedRange parent_cap = {} \<or> p = parent; untypedRange c \<noteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c = untypedRange parent_cap \<longrightarrow> parent \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' parent m \<and> usableUntypedRange parent_cap = {} \<or> p = parent; untypedRange c \<noteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange parent_cap = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (5 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> untypedRange parent_cap
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<subset> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 5. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<subset> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<subset> untypedRange parent_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<subset> untypedRange parent_cap; p \<in> descendants_of' parent m; untypedRange c \<inter> usableUntypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<subset> untypedRange parent_cap; m \<turnstile> parent \<rightarrow> p; untypedRange c \<inter> usableUntypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<subset> untypedRange parent_cap; untypedRange c \<inter> usableUntypedRange parent_cap = {}; capRange c \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<subset> untypedRange parent_cap; untypedRange c \<inter> usableUntypedRange parent_cap = {}; capRange c \<inter> capRange c' = {}; isUntypedCap c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); capRange c' \<subseteq> untypedRange parent_cap; untypedRange parent_cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<noteq> untypedRange parent_cap; untypedRange c \<inter> untypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c' x node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); untyped_mdb' m; untyped_inc' m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal:
No subgoals!