theory CSpace_AI

lemma untyped_inc_simple:
  assumes u: "untyped_inc m cs"
  assumes src: "cs src = Some c"
  assumes al:  "cap_aligned c"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes ut: "untyped_range cap = untyped_range c \<or> \<not>is_untyped_cap cap"
  assumes ut': "is_untyped_cap cap \<longrightarrow> is_untyped_cap c"
  assumes dsc: "is_untyped_cap cap \<longrightarrow> descendants_of src m = {}"
  assumes usable:"is_untyped_cap cap \<longrightarrow> is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}"
  shows "untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" proof - have  no_usage:"\<And>p c'. is_untyped_cap cap \<longrightarrow> cs p = Some c' \<longrightarrow> untyped_range c = untyped_range c' \<longrightarrow> usable_untyped_range c' = {}" using src u unfolding untyped_inc_def apply (erule_tac x = src in allE) apply (intro impI) apply (erule_tac x = p in allE) apply (case_tac "is_untyped_cap c") apply simp apply (case_tac "is_untyped_cap c'") apply simp using dsc ut usable apply clarsimp apply (elim disjE) apply clarsimp+ using al apply (case_tac c',simp_all add:is_cap_simps untyped_range_non_empty) using ut' apply (clarsimp simp:is_cap_simps) done from ut ut' dsc dst show ?thesis using u src desc unfolding untyped_inc_def apply (simp del: fun_upd_apply split_paired_All) apply (intro allI) apply (case_tac "p = dest") apply (case_tac "p' = dest") apply (clarsimp simp:src dst) apply (case_tac "p'=src") apply (erule_tac x=src in allE) apply (erule_tac x=p' in allE) apply (cut_tac p = src and c' = c in no_usage) apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child) apply (erule_tac x=src in allE) apply (erule_tac x=p' in allE) apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child) apply (erule_tac x=p in allE) apply (case_tac "p'=dest") apply (case_tac "p'=src") apply (erule_tac x=src in allE) apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child) apply (erule_tac x=src in allE) apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child) apply (cut_tac p = "(a,b)" and c' = ca in no_usage) apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child) apply (case_tac "p' = src") apply (erule_tac x = src in allE) apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child) apply (erule_tac x = p' in allE) apply (clarsimp simp del:split_paired_All simp: descendants_child) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (state)
goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<And>p c'. is_untyped_cap cap \<longrightarrow> cs p = Some c' \<longrightarrow> untyped_range c = untyped_range c' \<longrightarrow> usable_untyped_range c' = {} proof (prove)
using this:
cs src = Some c
untyped_inc m cs

goal (1 subgoal):
 1. \<And>p c'. is_untyped_cap cap \<longrightarrow> cs p = Some c' \<longrightarrow> untyped_range c = untyped_range c' \<longrightarrow> usable_untyped_range c' = {} proof (prove)
using this:
cs src = Some c
\<forall>p p' c c'. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')

goal (1 subgoal):
 1. \<And>p c'. is_untyped_cap cap \<longrightarrow> cs p = Some c' \<longrightarrow> untyped_range c = untyped_range c' \<longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (1 subgoal):
 1. \<And>p c'. \<lbrakk>cs src = Some c; \<forall>p' c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> src = p')\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> cs p = Some c' \<longrightarrow> untyped_range c = untyped_range c' \<longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (1 subgoal):
 1. \<And>p c'. \<lbrakk>cs src = Some c; \<forall>p' c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> src = p'); is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (1 subgoal):
 1. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p)\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (2 subgoals):
 1. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (2 subgoals):
 1. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (3 subgoals):
 1. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c; is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c; \<not> is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 3. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (3 subgoals):
 1. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c; is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c; \<not> is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 3. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
using this:
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}
untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap
is_untyped_cap cap \<longrightarrow> is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}

goal (3 subgoals):
 1. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c; is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c; \<not> is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 3. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (3 subgoals):
 1. \<And>a b c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs (a, b) = Some c'; untyped_range c = untyped_range c'; src \<in> descendants_of (a, b) m \<and> usable_untyped_range c' = {} \<or> src = (a, b); is_untyped_cap c; is_untyped_cap c'; descendants_of src m = {}; untyped_range cap = untyped_range c'; usable_untyped_range c = {}\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c; \<not> is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 3. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (4 subgoals):
 1. \<And>a b c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs (a, b) = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c; is_untyped_cap c'; descendants_of src m = {}; untyped_range cap = untyped_range c'; usable_untyped_range c = {}; src \<in> descendants_of (a, b) m \<and> usable_untyped_range c' = {}\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>a b c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs (a, b) = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c; is_untyped_cap c'; descendants_of src m = {}; untyped_range cap = untyped_range c'; usable_untyped_range c = {}; src = (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 3. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p; is_untyped_cap c; \<not> is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 4. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (2 subgoals):
 1. \<And>a b c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs (a, b) = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c; \<not> is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
using this:
cap_aligned c

goal (2 subgoals):
 1. \<And>a b c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs (a, b) = Some c'; untyped_range c = untyped_range c'; is_untyped_cap c; \<not> is_untyped_cap c'\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {}
 2. \<And>p c'. \<lbrakk>cs src = Some c; is_untyped_cap cap; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>c c'. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p m \<and> usable_untyped_range c' = {} \<or> src = p); \<not> is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal (1 subgoal):
 1. \<And>p c'. \<lbrakk>cs src = Some c; \<exists>dev r bits f. cap = UntypedCap dev r bits f; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; cap_aligned c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
using this:
is_untyped_cap cap \<longrightarrow> is_untyped_cap c

goal (1 subgoal):
 1. \<And>p c'. \<lbrakk>cs src = Some c; \<exists>dev r bits f. cap = UntypedCap dev r bits f; cs p = Some c'; untyped_range c = untyped_range c'; \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; cap_aligned c\<rbrakk> \<Longrightarrow> usable_untyped_range c' = {} proof (prove)
goal:
No subgoals! proof (state)
this:
is_untyped_cap cap \<longrightarrow> cs ?p = Some ?c' \<longrightarrow> untyped_range c = untyped_range ?c' \<longrightarrow> usable_untyped_range ?c' = {}

goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (chain)
picking this:
untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap
is_untyped_cap cap \<longrightarrow> is_untyped_cap c
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}
cs dest = Some NullCap proof (prove)
using this:
untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap
is_untyped_cap cap \<longrightarrow> is_untyped_cap c
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}
cs dest = Some NullCap

goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
using this:
untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap
is_untyped_cap cap \<longrightarrow> is_untyped_cap c
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}
cs dest = Some NullCap
untyped_inc m cs
cs src = Some c
descendants_of dest m = {}

goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
using this:
untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap
is_untyped_cap cap \<longrightarrow> is_untyped_cap c
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}
cs dest = Some NullCap
\<forall>p p' c c'. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')
cs src = Some c
descendants_of dest m = {}

goal (1 subgoal):
 1. \<forall>p p' c c'. (cs(dest \<mapsto> cap)) p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}\<rbrakk> \<Longrightarrow> \<forall>p p' c. (cs(dest \<mapsto> cap)) p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' = dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 3. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' = src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 3. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' = src; \<forall>p' c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 3. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' = src; \<forall>c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 3. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' = src; \<forall>c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> src = p')); is_untyped_cap cap \<longrightarrow> cs src = Some c \<longrightarrow> untyped_range c = untyped_range c \<longrightarrow> usable_untyped_range c = {}\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 3. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' \<noteq> src; \<forall>p' c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p = dest; p' \<noteq> dest; p' \<noteq> src; \<forall>c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of src m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; \<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some c; descendants_of dest m = {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p'))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' = dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' = dest; p' = src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' = dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 3. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; p' = dest; p' = src; \<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs src = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range c' = {} \<or> p = src))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' = dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 3. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' = dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; p' = dest; p' \<noteq> src; \<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs src = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range c' = {} \<or> p = src))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ca. \<lbrakk>cs (aa, ba) = Some NullCap; cs src = Some c; descendants_of (aa, ba) m = {}; dest = (aa, ba); a = aa \<longrightarrow> b \<noteq> ba; cs (a, b) = Some ca; is_untyped_cap ca; is_untyped_cap cap; untyped_range cap = untyped_range c; is_untyped_cap c; descendants_of src m = {}; untyped_range ca = untyped_range c; src \<in> descendants_of (a, b) m \<and> usable_untyped_range ca = {} \<or> (a, b) = src\<rbrakk> \<Longrightarrow> (aa, ba) \<in> (if src \<in> descendants_of (a, b) m \<or> (a, b) = src then descendants_of (a, b) m \<union> {(aa, ba)} else descendants_of (a, b) m) \<and> usable_untyped_range ca = {}
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ca. \<lbrakk>cs (aa, ba) = Some NullCap; cs src = Some c; descendants_of (aa, ba) m = {}; dest = (aa, ba); a = aa \<longrightarrow> b \<noteq> ba; cs (a, b) = Some ca; is_untyped_cap ca; is_untyped_cap cap; untyped_range cap = untyped_range c; is_untyped_cap c; descendants_of src m = {}; untyped_range ca = untyped_range c; src \<in> descendants_of (a, b) m \<and> usable_untyped_range ca = {} \<or> (a, b) = src; is_untyped_cap cap \<longrightarrow> cs (a, b) = Some ca \<longrightarrow> untyped_range c = untyped_range ca \<longrightarrow> usable_untyped_range ca = {}\<rbrakk> \<Longrightarrow> (aa, ba) \<in> (if src \<in> descendants_of (a, b) m \<or> (a, b) = src then descendants_of (a, b) m \<union> {(aa, ba)} else descendants_of (a, b) m) \<and> usable_untyped_range ca = {}
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest; p' = src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; p' \<noteq> dest; p' = src; \<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs src = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of src m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> src \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> src \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range c' = {} \<or> p = src))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')); p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca. \<lbrakk>untyped_range cap = untyped_range c \<or> \<not> is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> is_untyped_cap c; is_untyped_cap cap \<longrightarrow> descendants_of src m = {}; cs dest = Some NullCap; cs src = Some c; descendants_of dest m = {}; p \<noteq> dest; p' \<noteq> dest; p' \<noteq> src; \<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p'))\<rbrakk> \<Longrightarrow> (cs(dest \<mapsto> cap)) p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> (\<forall>c'. (cs(dest \<mapsto> cap)) p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p (m(dest \<mapsto> src)) \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' (m(dest \<mapsto> src)) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal:
No subgoals! proof (state)
this:
untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))

goal:
No subgoals!