theory CSpace_R

lemma untyped_inc_n:
  assumes c': "capAligned c'"
  shows "untyped_inc' n" using untyped_inc not_untyped [OF c'] apply (clarsimp simp add: untyped_inc'_def descendants split del: if_split) apply (drule n_cap)+ apply (clarsimp split: if_split_asm) apply (simp add: descendants_of'_def untyped_c') apply (case_tac "p = dest") apply (clarsimp simp: untyped_c') apply simp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc' n proof (prove)
using this:
untyped_inc' m
\<not> isUntypedCap src_cap

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