theory CSpace_R

lemma caps_contained' [simp]:
  "caps_contained' n'" using src dest capRange_c' utCapRange_c' apply (clarsimp simp: caps_contained'_def) apply (drule n'_cap)+ apply clarsimp apply (clarsimp split: if_split_asm) apply (drule capRange_untyped) apply simp apply (drule capRange_untyped) apply clarsimp apply (cases "isUntypedCap src_cap") prefer 2 apply (drule_tac p=p and p'=src in caps_containedD', assumption+) apply blast apply (rule caps_contained) apply blast apply (frule capRange_untyped) apply (drule (3) untyped_incD', rule untyped_inc) apply (clarsimp simp: ut_descendants) apply blast apply (drule (3) caps_containedD', rule caps_contained) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_contained' n' proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)
capRange c' \<subseteq> capRange src_cap
capRange c' \<subseteq> untypedRange src_cap

goal (1 subgoal):
 1. caps_contained' n' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c'a n'a x. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; n' p = Some (CTE c n); n' p' = Some (CTE c'a n'a); \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c'a n' x. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; \<exists>node'. if p = dest then c = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE c node'); \<exists>node'. if p' = dest then c'a = c' \<and> m p' = Some (CTE dest_cap node') else m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; if p = dest then c = c' \<and> dest_node = node' else m p = Some (CTE c node'); if p' = dest then c'a = c' \<and> dest_node = node'a else m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p' c'a x node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 3. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; x \<in> capRange c'; isUntypedCap c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p' c'a x node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 3. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; x \<in> capRange c'a; p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p' c'a x node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; x \<in> capRange c'a; p' \<noteq> dest; m p' = Some (CTE c'a node'a); isUntypedCap c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c'
 2. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (5 subgoals):
 1. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> capRange src_cap \<inter> untypedRange c \<noteq> {}
 2. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> caps_contained' m
 3. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; \<not> isUntypedCap src_cap; capRange src_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 5. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> caps_contained' m
 2. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; \<not> isUntypedCap src_cap; capRange src_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; \<not> isUntypedCap src_cap; capRange src_cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap; isUntypedCap c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap; isUntypedCap c; (untypedRange src_cap \<subseteq> untypedRange c \<or> untypedRange c \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c = {}) \<and> (untypedRange src_cap \<subset> untypedRange c \<longrightarrow> src \<in> descendants_of' p m \<and> untypedRange src_cap \<inter> usableUntypedRange c = {}) \<and> (untypedRange c \<subset> untypedRange src_cap \<longrightarrow> p \<in> descendants_of' src m \<and> untypedRange c \<inter> usableUntypedRange src_cap = {}) \<and> (untypedRange src_cap = untypedRange c \<longrightarrow> p \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {} \<or> src \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> src = p)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c x node'. \<lbrakk>m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> dest; m p = Some (CTE c node'); isUntypedCap src_cap; isUntypedCap c; untypedRange src_cap \<subseteq> untypedRange c \<or> untypedRange c = untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c = {}; untypedRange src_cap \<subset> untypedRange c \<longrightarrow> src \<in> descendants_of' p m \<and> untypedRange src_cap \<inter> usableUntypedRange c = {}; \<not> untypedRange c \<subset> untypedRange src_cap; untypedRange src_cap = untypedRange c \<longrightarrow> src \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> src = p\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; m p = Some (CTE c node'); p' \<noteq> dest; m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c'a x node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); capRange c' \<subseteq> capRange src_cap; capRange c' \<subseteq> untypedRange src_cap; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'a; p \<noteq> dest; p' \<noteq> dest; m p' = Some (CTE c'a node'a); capRange c'a \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal:
No subgoals!