theory CSpace_R

lemma ut_mdb' [simp]:
  "untyped_mdb' n'" using src dest utRange_c' capRange_c' utCapRange_c' apply (clarsimp simp: untyped_mdb'_def) apply (drule n'_cap)+ apply (clarsimp simp: descendants') apply (clarsimp split: if_split_asm) apply (cases "isUntypedCap src_cap") prefer 2 apply (drule_tac p=p and p'=src and m=m in untyped_mdbD', assumption+) apply blast apply (rule untyped_mdb) apply simp apply (frule ut_descendants) apply (drule (3) untyped_incD', rule untyped_inc) apply clarsimp apply blast apply (fastforce elim: untyped_mdbD' intro!: untyped_mdb) done

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

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