theory Untyped_R

lemma untyped_mdb_n' [simp]: "untyped_mdb' n'" using untyped_mdb capRange_ut untyped_inc apply (clarsimp simp: untyped_mdb'_def descendants_of'_def) apply (drule n'_cap)+ apply (simp add: parency_n') apply (simp split: if_split_asm) apply clarsimp apply (erule_tac x=parent in allE) apply (simp add: parent is_untyped) apply (erule_tac x=p' in allE) apply simp apply (frule untypedCapRange) apply (drule untypedRange_c') apply (erule impE, blast) apply (drule (1) rangeD) apply simp apply clarsimp apply (thin_tac "All P" for P) apply (simp add: untyped_inc'_def) apply (erule_tac x=parent in allE) apply (erule_tac x=p in allE) apply (simp add: parent is_untyped) apply (clarsimp simp: descendants_of'_def) apply (case_tac "untypedRange parent_cap = untypedRange c") apply simp apply (elim disjE conjE) apply (drule (1) rangeD) apply (drule untypedCapRange) apply simp apply blast apply simp apply (erule disjE) apply clarsimp apply (erule disjE) apply (simp add: psubsetI) apply (elim conjE) apply (drule (1) rangeD) apply (drule untypedCapRange) apply simp apply blast apply blast apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb' n' proof (prove)
using this:
untyped_mdb' m
capRange c' \<subseteq> untypedRange parent_cap
untyped_inc' m

goal (1 subgoal):
 1. untyped_mdb' n' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c'a n'a. \<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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; n' p = Some (CTE c n); isUntypedCap c; n' p' = Some (CTE c'a n'a); \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c'a n'a. \<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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; 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> n' \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c'a. \<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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; 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> (m \<turnstile> p \<rightarrow> parent \<longrightarrow> m \<turnstile> p \<rightarrow> p' \<or> p' = site) \<and> (p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' \<or> p' = site) \<and> (\<not> m \<turnstile> p \<rightarrow> parent \<and> p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> p') proof (prove)
goal (3 subgoals):
 1. \<And>p p' c'a. \<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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c'; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; p = site; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c'; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c'; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); \<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> m \<turnstile> parent \<rightarrow> p')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c'; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); \<forall>p' c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange parent_cap \<noteq> {} \<longrightarrow> m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c'; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); \<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange parent_cap \<noteq> {} \<longrightarrow> m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c'; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); capRange c'a \<inter> untypedRange parent_cap \<noteq> {} \<longrightarrow> m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c'; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); capRange c'a \<inter> untypedRange parent_cap \<noteq> {} \<longrightarrow> m \<turnstile> parent \<rightarrow> p'; capRange c' = untypedRange c'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); capRange c'a \<inter> untypedRange parent_cap \<noteq> {} \<longrightarrow> m \<turnstile> parent \<rightarrow> p'; capRange c' = untypedRange c'; untypedRange c' \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); capRange c' = untypedRange c'; untypedRange c' \<subseteq> untypedRange parent_cap; m \<turnstile> parent \<rightarrow> p'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; m site = Some (CTE capability.NullCap site_node); p' \<noteq> site; m p' = Some (CTE c'a node'); capRange c' = untypedRange c'; untypedRange c' \<subseteq> untypedRange parent_cap; capRange c'a \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p p' c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' = site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent \<or> p = parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; \<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> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; \<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> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> parent \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' parent m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' parent m \<and> usableUntypedRange c = {} \<or> parent \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> parent = p'))\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; \<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> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p \<in> descendants_of' parent m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p \<in> descendants_of' parent m \<and> usableUntypedRange c = {} \<or> parent \<in> descendants_of' p m \<and> usableUntypedRange c' = {} \<or> parent = p))\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; (untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}) \<and> (untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> parent \<in> descendants_of' p m \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}) \<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 = untypedRange c \<longrightarrow> p \<in> descendants_of' parent m \<and> usableUntypedRange parent_cap = {} \<or> parent \<in> descendants_of' p m \<and> usableUntypedRange c = {})\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap = untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap = untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (4 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; m \<turnstile> parent \<rightarrow> p; usableUntypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; m \<turnstile> p \<rightarrow> parent; usableUntypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 4. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (4 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; usableUntypedRange parent_cap = {}; capRange c \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; m \<turnstile> p \<rightarrow> parent; usableUntypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 4. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (4 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; usableUntypedRange parent_cap = {}; capRange c \<inter> capRange c' = {}; capRange c = untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; m \<turnstile> p \<rightarrow> parent; usableUntypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 4. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (4 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; usableUntypedRange parent_cap = {}; untypedRange c \<inter> capRange c' = {}; capRange c = untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; m \<turnstile> p \<rightarrow> parent; usableUntypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 4. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange c; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap = untypedRange c; m \<turnstile> p \<rightarrow> parent; usableUntypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange parent_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange c \<subseteq> untypedRange parent_cap \<or> untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange c \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange c \<subseteq> untypedRange parent_cap\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange c \<subseteq> untypedRange parent_cap; m \<turnstile> parent \<rightarrow> p; untypedRange c \<inter> usableUntypedRange parent_cap = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange c \<subseteq> untypedRange parent_cap; untypedRange c \<inter> usableUntypedRange parent_cap = {}; capRange c \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange c \<subseteq> untypedRange parent_cap; untypedRange c \<inter> usableUntypedRange parent_cap = {}; capRange c \<inter> capRange c' = {}; capRange c = untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange c \<subseteq> untypedRange parent_cap; untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange c \<inter> capRange c' = {}; capRange c = untypedRange c\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 3. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>p c node'. \<lbrakk>capRange c' \<subseteq> untypedRange parent_cap; isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> site; m p = Some (CTE c node'); m site = Some (CTE capability.NullCap site_node); p \<noteq> parent; untypedRange parent_cap \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> parent \<and> untypedRange parent_cap \<inter> usableUntypedRange c = {}; untypedRange c \<subset> untypedRange parent_cap \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange parent_cap = {}; untypedRange parent_cap = untypedRange c \<longrightarrow> m \<turnstile> parent \<rightarrow> p \<and> usableUntypedRange parent_cap = {} \<or> m \<turnstile> p \<rightarrow> parent \<and> usableUntypedRange c = {}; untypedRange parent_cap \<noteq> untypedRange c; untypedRange parent_cap \<inter> untypedRange c = {}\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c'a 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> m \<turnstile> p \<rightarrow> p'); capRange c' \<subseteq> untypedRange parent_cap; untyped_inc' m; isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p \<noteq> site; p' \<noteq> site; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p = parent \<longrightarrow> m \<turnstile> parent \<rightarrow> p' proof (prove)
goal:
No subgoals!