theory CSpace_AI

lemma untyped_inc:
  assumes ut: "untyped_inc m cs"
  assumes s: "cs src = Some src_cap"
  assumes d: "cs dest = Some cap.NullCap"
  assumes c: "weak_derived cap src_cap"
  shows "untyped_inc m' (cs (dest \<mapsto> cap, src \<mapsto> cap.NullCap))" proof - from c have "is_untyped_cap cap = is_untyped_cap src_cap"
       "untyped_range cap = untyped_range src_cap"
       "is_untyped_cap cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap" by (auto simp: copy_of_def same_object_as_def is_cap_simps weak_derived_def
             split: if_split_asm cap.splits) with ut s d show ?thesis apply (simp add: untyped_inc_def descendants del: split_paired_All split del: if_split) apply (intro allI) apply (case_tac "p = src") apply (simp  del: split_paired_All split del: if_split) apply (simp  del: split_paired_All split del: if_split) apply (case_tac "p = dest") apply (simp del: split_paired_All split del: if_split) apply (case_tac "p' = src") apply (simp del: split_paired_All split del: if_split)+ apply (case_tac "p' = dest") apply (simp del:split_paired_All split del:if_split)+ apply (intro impI allI conjI) apply ((erule_tac x=src in allE,erule_tac x=p' in allE,simp)+)[5] apply (erule_tac x=src in allE) apply (erule_tac x=p' in allE) apply simp apply (intro conjI impI) apply (simp del:split_paired_All split del:if_split)+ apply (case_tac "p' = src") apply (simp del: split_paired_All split del: if_split)+ apply (case_tac "p' = dest") apply (simp del:split_paired_All split del:if_split)+ apply (intro impI allI conjI) apply (erule_tac x=p in allE,erule_tac x=src in allE) apply simp apply (intro conjI impI) apply (simp del:split_paired_All split del:if_split)+ apply (intro conjI impI allI) apply (erule_tac x=p in allE,erule_tac x=p' in allE) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) proof (state)
goal (1 subgoal):
 1. untyped_inc m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) proof (chain)
picking this:
weak_derived cap src_cap proof (prove)
using this:
weak_derived cap src_cap

goal (1 subgoal):
 1. is_untyped_cap cap = is_untyped_cap src_cap &&& untyped_range cap = untyped_range src_cap &&& is_untyped_cap cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap proof (state)
this:
is_untyped_cap cap = is_untyped_cap src_cap
untyped_range cap = untyped_range src_cap
is_untyped_cap cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap

goal (1 subgoal):
 1. untyped_inc m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) proof (chain)
picking this:
untyped_inc m cs
cs src = Some src_cap
cs dest = Some NullCap
is_untyped_cap cap = is_untyped_cap src_cap
untyped_range cap = untyped_range src_cap
is_untyped_cap cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap proof (prove)
using this:
untyped_inc m cs
cs src = Some src_cap
cs dest = Some NullCap
is_untyped_cap cap = is_untyped_cap src_cap
untyped_range cap = untyped_range src_cap
is_untyped_cap cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap

goal (1 subgoal):
 1. untyped_inc m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap\<rbrakk> \<Longrightarrow> \<forall>p p' c. (if p = src then Some NullCap else (cs(dest \<mapsto> cap)) p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap\<rbrakk> \<Longrightarrow> (if p = src then Some NullCap else (cs(dest \<mapsto> cap)) p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = src\<rbrakk> \<Longrightarrow> (if p = src then Some NullCap else (cs(dest \<mapsto> cap)) p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src\<rbrakk> \<Longrightarrow> (if p = src then Some NullCap else (cs(dest \<mapsto> cap)) p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src\<rbrakk> \<Longrightarrow> (if p = src then Some NullCap else (cs(dest \<mapsto> cap)) p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = src then {} else if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest\<rbrakk> \<Longrightarrow> cap = c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> dest \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> dest \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> dest = p'))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' = src\<rbrakk> \<Longrightarrow> cap = c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> dest \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> dest \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> dest = p'))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> cap = c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> dest \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> dest \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> dest = p'))
 3. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> cap = c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some c else 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> dest \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> dest \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> dest = p'))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' = dest\<rbrakk> \<Longrightarrow> cap = c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some c else 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> dest \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> dest \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> dest = p'))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cap = c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some c else 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> dest \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> dest \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> dest = p'))
 3. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cap = 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> dest \<in> (if src \<in> descendants_of p' m then {dest} else {}) \<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> dest \<in> (if src \<in> descendants_of p' m then {dest} else {}) \<and> usable_untyped_range c' = {}))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (7 subgoals):
 1. \<And>p p' c c'. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'\<rbrakk> \<Longrightarrow> untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}
 2. \<And>p p' c c'. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c \<subset> untyped_range c'\<rbrakk> \<Longrightarrow> dest \<in> (if src \<in> descendants_of p' m then {dest} else {})
 3. \<And>p p' c c'. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c \<subset> untyped_range c'\<rbrakk> \<Longrightarrow> untyped_range c \<inter> usable_untyped_range c' = {}
 4. \<And>p p' c c'. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c' \<subset> untyped_range c\<rbrakk> \<Longrightarrow> p' \<in> descendants_of src m
 5. \<And>p p' c c'. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c' \<subset> untyped_range c\<rbrakk> \<Longrightarrow> untyped_range c' \<inter> usable_untyped_range c = {}
 6. \<And>p p' c c'. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range c'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> dest \<in> (if src \<in> descendants_of p' m then {dest} else {}) \<and> usable_untyped_range c' = {}
 7. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c c'. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range c'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> dest \<in> (if src \<in> descendants_of p' m then {dest} else {}) \<and> usable_untyped_range c' = {}
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c c'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range c'; \<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> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> dest \<in> (if src \<in> descendants_of p' m then {dest} else {}) \<and> usable_untyped_range c' = {}
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c c'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range c'; \<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> p' \<in> descendants_of src m \<and> usable_untyped_range c = {} \<or> dest \<in> (if src \<in> descendants_of p' m then {dest} else {}) \<and> usable_untyped_range c' = {}
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c c'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap src_cap; untyped_range c' = untyped_range src_cap; usable_untyped_range c = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range src_cap; p' \<in> descendants_of src m \<and> usable_untyped_range src_cap = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {}\<rbrakk> \<Longrightarrow> (src \<in> descendants_of p' m \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range src_cap = {} \<or> usable_untyped_range c' = {}) \<and> (src \<notin> descendants_of p' m \<longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range src_cap = {})
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (4 subgoals):
 1. \<And>p p' c c'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap src_cap; untyped_range c' = untyped_range src_cap; usable_untyped_range c = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range src_cap; p' \<in> descendants_of src m \<and> usable_untyped_range src_cap = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {}; src \<in> descendants_of p' m\<rbrakk> \<Longrightarrow> p' \<in> descendants_of src m \<and> usable_untyped_range src_cap = {} \<or> usable_untyped_range c' = {}
 2. \<And>p p' c c'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap src_cap; untyped_range c' = untyped_range src_cap; usable_untyped_range c = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range src_cap; p' \<in> descendants_of src m \<and> usable_untyped_range src_cap = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {}; src \<notin> descendants_of p' m\<rbrakk> \<Longrightarrow> p' \<in> descendants_of src m
 3. \<And>p p' c c'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap src_cap; untyped_range c' = untyped_range src_cap; usable_untyped_range c = usable_untyped_range src_cap; p = dest; p' \<noteq> src; p' \<noteq> dest; cap = c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range src_cap; p' \<in> descendants_of src m \<and> usable_untyped_range src_cap = {} \<or> src \<in> descendants_of p' m \<and> usable_untyped_range c' = {}; src \<notin> descendants_of p' m\<rbrakk> \<Longrightarrow> usable_untyped_range src_cap = {}
 4. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (if p = dest then Some cap else cs p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> (if p = dest then descendants_of src m else descendants_of p m - {src} \<union> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> p' \<noteq> src \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<and> p' \<noteq> src \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' = src\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> p' \<noteq> src \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<and> p' \<noteq> src \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = src then Some NullCap else (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> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<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> p' \<noteq> src \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<and> p' \<noteq> src \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = src then {} else if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some cap else 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> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' = dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some cap else 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> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p'))
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some cap else 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> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' = dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> untyped_range c = untyped_range src_cap \<longrightarrow> dest \<in> (if src \<in> descendants_of p m then {dest} else {}) \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some cap else 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> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; cs p = Some c; is_untyped_cap c; is_untyped_cap src_cap; untyped_range c = untyped_range src_cap\<rbrakk> \<Longrightarrow> dest \<in> (if src \<in> descendants_of p m then {dest} else {}) \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some cap else 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> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; cs p = Some c; is_untyped_cap c; is_untyped_cap src_cap; untyped_range c = untyped_range src_cap; \<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> dest \<in> (if src \<in> descendants_of p m then {dest} else {}) \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some cap else 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> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap cap; untyped_range cap = untyped_range src_cap; usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; cs p = Some c; is_untyped_cap c; is_untyped_cap src_cap; untyped_range c = untyped_range src_cap; src \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}\<rbrakk> \<Longrightarrow> (src \<in> descendants_of p m \<longrightarrow> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}) \<and> (src \<notin> descendants_of p m \<longrightarrow> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {})
 2. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some cap else 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> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (4 subgoals):
 1. \<And>p p' c. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap cap; untyped_range cap = untyped_range src_cap; usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; cs p = Some c; is_untyped_cap c; is_untyped_cap src_cap; untyped_range c = untyped_range src_cap; src \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}
 2. \<And>p p' c. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap cap; untyped_range cap = untyped_range src_cap; usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; cs p = Some c; is_untyped_cap c; is_untyped_cap src_cap; untyped_range c = untyped_range src_cap; src \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}; src \<notin> descendants_of p m\<rbrakk> \<Longrightarrow> p \<in> descendants_of src m
 3. \<And>p p' c. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap cap; untyped_range cap = untyped_range src_cap; usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; cs p = Some c; is_untyped_cap c; is_untyped_cap src_cap; untyped_range c = untyped_range src_cap; src \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of src m \<and> usable_untyped_range src_cap = {}; src \<notin> descendants_of p m\<rbrakk> \<Longrightarrow> usable_untyped_range src_cap = {}
 4. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if p' = dest then Some cap else 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> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> p \<in> (if p' = dest then descendants_of src m else descendants_of p' m - {src} \<union> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> 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 = untyped_range c' \<longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> (p \<in> descendants_of p' m \<or> p \<in> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c'. \<lbrakk>\<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 src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; cs p = Some c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range c'\<rbrakk> \<Longrightarrow> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> (p \<in> descendants_of p' m \<or> p \<in> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; is_untyped_cap cap = is_untyped_cap src_cap; untyped_range cap = untyped_range src_cap; is_untyped_cap src_cap \<longrightarrow> usable_untyped_range cap = usable_untyped_range src_cap; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; cs p = Some c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_range c = untyped_range c'; \<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> (p' \<in> descendants_of p m \<or> p' \<in> (if src \<in> descendants_of p m then {dest} else {})) \<and> usable_untyped_range c = {} \<or> (p \<in> descendants_of p' m \<or> p \<in> (if src \<in> descendants_of p' m then {dest} else {})) \<and> usable_untyped_range c' = {} \<or> p = p' proof (prove)
goal:
No subgoals! proof (state)
this:
untyped_inc m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap))

goal:
No subgoals!