theory CSpace_R

lemma untyped_mdb_n:
  shows "untyped_mdb' n" using untyped_mdb apply (clarsimp simp add: untyped_mdb'_def descendants split del: if_split) apply (drule n_cap)+ apply (clarsimp split: if_split_asm) apply (erule disjE, clarsimp) apply (simp add: descendants_of'_def) apply (erule_tac x=p in allE) apply (erule_tac x=src in allE) apply (simp add: src untyped_c' capRange_c') apply (erule disjE) apply clarsimp apply (simp add: descendants_of'_def untyped_c') apply (erule_tac x=src in allE) apply (erule_tac x=p' in allE) apply (fastforce simp: src dest: untyped_no_parent) apply (case_tac "p=src", simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb' n proof (prove)
using this:
untyped_mdb' m

goal (1 subgoal):
 1. untyped_mdb' n proof (prove)
goal (1 subgoal):
 1. \<And>p p' c na c' n'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); n p = Some (CTE c na); isUntypedCap c; n p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p' \<in> (if src \<in> descendants_of' p m \<or> p = src then insert dest (descendants_of' p m) else descendants_of' p m) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c'a n'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); 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> (if src \<in> descendants_of' p m \<or> p = src then insert dest (descendants_of' p m) else descendants_of' p m) proof (prove)
goal (2 subgoals):
 1. \<And>p c node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p = dest \<longrightarrow> c = c' \<and> node'a = node'; p = dest \<or> m p = Some (CTE c node'); m dest = Some (CTE dest_cap node'a); 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>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); p = dest \<or> m p = Some (CTE c node'); 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' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p = dest \<longrightarrow> c = c' \<and> node'a = node'; m dest = Some (CTE dest_cap node'a); src \<notin> descendants_of' p m; p \<noteq> src; m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> dest \<in> descendants_of' p m
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); p = dest \<or> m p = Some (CTE c node'); 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' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p = dest \<longrightarrow> c = c' \<and> node'a = node'; m dest = Some (CTE dest_cap node'a); \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); p = dest \<or> m p = Some (CTE c node'); 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' node'a. \<lbrakk>isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p = dest \<longrightarrow> c = c' \<and> node'a = node'; m dest = Some (CTE dest_cap node'a); \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; m p = Some (CTE c node'); \<forall>p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); p = dest \<or> m p = Some (CTE c node'); 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' node'a. \<lbrakk>isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p = dest \<longrightarrow> c = c' \<and> node'a = node'; m dest = Some (CTE dest_cap node'a); \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> src; m p = Some (CTE c node'); \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m src = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> src)\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); p = dest \<or> m p = Some (CTE c node'); 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>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); p = dest \<or> m p = Some (CTE c node'); 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 p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a); p = dest\<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)
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a); m p = Some (CTE c node')\<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'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c'; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c' \<noteq> {}; p' \<noteq> dest; m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' dest m
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a); m p = Some (CTE c node')\<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' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap src_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; p' \<noteq> dest; m dest = Some (CTE dest_cap node'); m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a); m p = Some (CTE c node')\<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' node'a. \<lbrakk>isUntypedCap src_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; p' \<noteq> dest; m dest = Some (CTE dest_cap node'); m p' = Some (CTE c' node'a); \<forall>p' c. (\<exists>n. m src = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> src \<rightarrow> p')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a); m p = Some (CTE c node')\<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' node'a. \<lbrakk>isUntypedCap src_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; p' \<noteq> dest; m dest = Some (CTE dest_cap node'); m p' = Some (CTE c' node'a); \<forall>c. (\<exists>n. m src = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> src \<rightarrow> p')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' c c'a node' node'a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a); m p = Some (CTE c node')\<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>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a); m p = Some (CTE c node')\<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>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<noteq> dest; p = dest \<longrightarrow> c = c' \<and> m dest = Some (CTE dest_cap node'); m p' = Some (CTE c'a node'a); m p = Some (CTE c node'); p \<noteq> src\<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!