theory CSpace1_R

lemma untyped_inc':
  assumes subeq: "\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte';isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow>
  usableUntypedRange (cteCap cte') \<subseteq> usableUntypedRange (cteCap cte)"
  shows "untyped_inc' m \<Longrightarrow> untyped_inc' m'" apply (clarsimp simp:untyped_inc'_def) apply (drule_tac x = p in spec) apply (drule_tac x = p' in spec) apply (frule iffD2[OF dom,OF domI],rotate_tac) apply (frule iffD2[OF dom,OF domI],rotate_tac) apply clarsimp apply (rename_tac cte cte') apply (case_tac cte) apply (rename_tac cap node) apply (case_tac cte') apply (drule_tac x = cap in spec) apply clarsimp apply (frule_tac x = p' in misc) apply assumption apply (frule_tac x = p in misc) apply assumption apply clarsimp apply (drule(1) subeq,simp)+ apply (subgoal_tac  "\<And>p p'. (p' \<in>descendants_of' p m) = (p' \<in> descendants_of' p m')") apply clarsimp apply (intro conjI impI) apply clarsimp apply (drule(1) disjoint_subset2[rotated],clarsimp+)+ apply (erule disjE) apply clarsimp+ apply (thin_tac "P" for P)+ apply (clarsimp simp: descendants_of'_def Invariants_H.subtree_def) apply (rule_tac f = "\<lambda>x. lfp x c" for c in arg_cong) apply (subgoal_tac "\<And>p p'. (m \<turnstile> p \<leadsto> p') = (m' \<turnstile> p \<leadsto> p')") apply (rule ext)+ apply clarsimp apply (subgoal_tac "(m \<turnstile> pa parentOf x) = (m' \<turnstile> pa parentOf x)") apply fastforce apply (rule parentOf_preserve[OF dom]) apply (simp add:misc sameRegion mdb_next mdb_next_rel_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc' m \<Longrightarrow> untyped_inc' m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n 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')); m' p = Some (CTE c n); isUntypedCap c; m' 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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>m' p = Some (CTE c n); isUntypedCap c; m' p' = Some (CTE c' n'); isUntypedCap c'; \<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> 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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>m' p = Some (CTE c n); isUntypedCap c; m' p' = Some (CTE c' n'); isUntypedCap c'; \<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> 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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; m' p' = Some (CTE c' n'); isUntypedCap c'; \<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')); p \<in> dom m; m' p = Some (CTE c n)\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; \<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')); p \<in> dom m; m' p = Some (CTE c n); p' \<in> dom m; 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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' y ya. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; \<forall>c. (\<exists>n. y = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ya = 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')); m' p = Some (CTE c n); isUntypedCap c; m p = Some y; m p' = Some ya\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cte cte'. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; \<forall>c. (\<exists>n. cte = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. cte' = 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')); m' p = Some (CTE c n); isUntypedCap c; m p = Some cte; m p' = Some cte'\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cte cte' x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; \<forall>c. (\<exists>n. cte = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. cte' = 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')); m' p = Some (CTE c n); isUntypedCap c; m p = Some cte; m p' = Some cte'; cte = CTE x1 x2\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cte cte' cap node. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; \<forall>c. (\<exists>n. cte = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. cte' = 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')); m' p = Some (CTE c n); isUntypedCap c; m p = Some cte; m p' = Some cte'; cte = CTE cap node\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cte cte' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; \<forall>c. (\<exists>n. cte = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. cte' = 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')); m' p = Some (CTE c n); isUntypedCap c; m p = Some cte; m p' = Some cte'; cte = CTE cap node; cte' = CTE x1 x2\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cte cte' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some cte; m p' = Some cte'; cte = CTE cap node; cte' = CTE x1 x2; (\<exists>n. cte = CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> (\<forall>c'. (\<exists>n'. cte' = CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange c' = {}) \<and> (untypedRange cap \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<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> 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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE cap node); m p' = Some (CTE x1 x2); isUntypedCap cap \<longrightarrow> isUntypedCap x1 \<longrightarrow> (untypedRange cap \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange x1 = {}) \<and> (untypedRange cap \<subset> untypedRange x1 \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<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> 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') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE cap node); m p' = Some (CTE x1 x2); isUntypedCap cap \<longrightarrow> isUntypedCap x1 \<longrightarrow> (untypedRange cap \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange x1 = {}) \<and> (untypedRange cap \<subset> untypedRange x1 \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p')\<rbrakk> \<Longrightarrow> m' p' = Some (?cte'41 p p' c n c' n' cap node x1 x2)
 2. \<And>p p' c n c' n' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE cap node); m p' = Some (CTE x1 x2); isUntypedCap cap \<longrightarrow> isUntypedCap x1 \<longrightarrow> (untypedRange cap \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange x1 = {}) \<and> (untypedRange cap \<subset> untypedRange x1 \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'); isUntypedCap (cteCap (CTE x1 x2)) = isUntypedCap (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> isNullCap (cteCap (CTE x1 x2)) = isNullCap (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> isReplyCap (cteCap (CTE x1 x2)) = isReplyCap (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> (isReplyCap (cteCap (CTE x1 x2)) \<longrightarrow> capReplyMaster (cteCap (CTE x1 x2)) = capReplyMaster (cteCap (?cte'41 p p' c n c' n' cap node x1 x2))) \<and> isNotificationCap (cteCap (CTE x1 x2)) = isNotificationCap (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> (isNotificationCap (cteCap (CTE x1 x2)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1 x2)) = capNtfnBadge (cteCap (?cte'41 p p' c n c' n' cap node x1 x2))) \<and> isEndpointCap (cteCap (CTE x1 x2)) = isEndpointCap (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> (isEndpointCap (cteCap (CTE x1 x2)) \<longrightarrow> capEPBadge (cteCap (CTE x1 x2)) = capEPBadge (cteCap (?cte'41 p p' c n c' n' cap node x1 x2))) \<and> untypedRange (cteCap (CTE x1 x2)) = untypedRange (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> capClass (cteCap (CTE x1 x2)) = capClass (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> isZombie (cteCap (CTE x1 x2)) = isZombie (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> isArchPageCap (cteCap (CTE x1 x2)) = isArchPageCap (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> capBits (cteCap (CTE x1 x2)) = capBits (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> global.capUntypedPtr (cteCap (CTE x1 x2)) = global.capUntypedPtr (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> capRange (cteCap (CTE x1 x2)) = capRange (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> isIRQControlCap (cteCap (CTE x1 x2)) = isIRQControlCap (cteCap (?cte'41 p p' c n c' n' cap node x1 x2)) \<and> cteMDBNode (CTE x1 x2) = cteMDBNode (?cte'41 p p' c n c' n' cap node x1 x2)\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE cap node); m p' = Some (CTE x1 x2); isUntypedCap cap \<longrightarrow> isUntypedCap x1 \<longrightarrow> (untypedRange cap \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange x1 = {}) \<and> (untypedRange cap \<subset> untypedRange x1 \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'); isUntypedCap (cteCap (CTE x1 x2)) = isUntypedCap (cteCap (CTE c' n')) \<and> isNullCap (cteCap (CTE x1 x2)) = isNullCap (cteCap (CTE c' n')) \<and> isReplyCap (cteCap (CTE x1 x2)) = isReplyCap (cteCap (CTE c' n')) \<and> (isReplyCap (cteCap (CTE x1 x2)) \<longrightarrow> capReplyMaster (cteCap (CTE x1 x2)) = capReplyMaster (cteCap (CTE c' n'))) \<and> isNotificationCap (cteCap (CTE x1 x2)) = isNotificationCap (cteCap (CTE c' n')) \<and> (isNotificationCap (cteCap (CTE x1 x2)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1 x2)) = capNtfnBadge (cteCap (CTE c' n'))) \<and> isEndpointCap (cteCap (CTE x1 x2)) = isEndpointCap (cteCap (CTE c' n')) \<and> (isEndpointCap (cteCap (CTE x1 x2)) \<longrightarrow> capEPBadge (cteCap (CTE x1 x2)) = capEPBadge (cteCap (CTE c' n'))) \<and> untypedRange (cteCap (CTE x1 x2)) = untypedRange (cteCap (CTE c' n')) \<and> capClass (cteCap (CTE x1 x2)) = capClass (cteCap (CTE c' n')) \<and> isZombie (cteCap (CTE x1 x2)) = isZombie (cteCap (CTE c' n')) \<and> isArchPageCap (cteCap (CTE x1 x2)) = isArchPageCap (cteCap (CTE c' n')) \<and> capBits (cteCap (CTE x1 x2)) = capBits (cteCap (CTE c' n')) \<and> global.capUntypedPtr (cteCap (CTE x1 x2)) = global.capUntypedPtr (cteCap (CTE c' n')) \<and> capRange (cteCap (CTE x1 x2)) = capRange (cteCap (CTE c' n')) \<and> isIRQControlCap (cteCap (CTE x1 x2)) = isIRQControlCap (cteCap (CTE c' n')) \<and> cteMDBNode (CTE x1 x2) = cteMDBNode (CTE c' n')\<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' \<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') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE cap node); m p' = Some (CTE x1 x2); isUntypedCap cap \<longrightarrow> isUntypedCap x1 \<longrightarrow> (untypedRange cap \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange x1 = {}) \<and> (untypedRange cap \<subset> untypedRange x1 \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'); isUntypedCap (cteCap (CTE x1 x2)) = isUntypedCap (cteCap (CTE c' n')) \<and> isNullCap (cteCap (CTE x1 x2)) = isNullCap (cteCap (CTE c' n')) \<and> isReplyCap (cteCap (CTE x1 x2)) = isReplyCap (cteCap (CTE c' n')) \<and> (isReplyCap (cteCap (CTE x1 x2)) \<longrightarrow> capReplyMaster (cteCap (CTE x1 x2)) = capReplyMaster (cteCap (CTE c' n'))) \<and> isNotificationCap (cteCap (CTE x1 x2)) = isNotificationCap (cteCap (CTE c' n')) \<and> (isNotificationCap (cteCap (CTE x1 x2)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1 x2)) = capNtfnBadge (cteCap (CTE c' n'))) \<and> isEndpointCap (cteCap (CTE x1 x2)) = isEndpointCap (cteCap (CTE c' n')) \<and> (isEndpointCap (cteCap (CTE x1 x2)) \<longrightarrow> capEPBadge (cteCap (CTE x1 x2)) = capEPBadge (cteCap (CTE c' n'))) \<and> untypedRange (cteCap (CTE x1 x2)) = untypedRange (cteCap (CTE c' n')) \<and> capClass (cteCap (CTE x1 x2)) = capClass (cteCap (CTE c' n')) \<and> isZombie (cteCap (CTE x1 x2)) = isZombie (cteCap (CTE c' n')) \<and> isArchPageCap (cteCap (CTE x1 x2)) = isArchPageCap (cteCap (CTE c' n')) \<and> capBits (cteCap (CTE x1 x2)) = capBits (cteCap (CTE c' n')) \<and> global.capUntypedPtr (cteCap (CTE x1 x2)) = global.capUntypedPtr (cteCap (CTE c' n')) \<and> capRange (cteCap (CTE x1 x2)) = capRange (cteCap (CTE c' n')) \<and> isIRQControlCap (cteCap (CTE x1 x2)) = isIRQControlCap (cteCap (CTE c' n')) \<and> cteMDBNode (CTE x1 x2) = cteMDBNode (CTE c' n')\<rbrakk> \<Longrightarrow> m' p = Some (?cte'43 p p' c n c' n' cap node x1 x2)
 2. \<And>p p' c n c' n' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE cap node); m p' = Some (CTE x1 x2); isUntypedCap cap \<longrightarrow> isUntypedCap x1 \<longrightarrow> (untypedRange cap \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange x1 = {}) \<and> (untypedRange cap \<subset> untypedRange x1 \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'); isUntypedCap (cteCap (CTE x1 x2)) = isUntypedCap (cteCap (CTE c' n')) \<and> isNullCap (cteCap (CTE x1 x2)) = isNullCap (cteCap (CTE c' n')) \<and> isReplyCap (cteCap (CTE x1 x2)) = isReplyCap (cteCap (CTE c' n')) \<and> (isReplyCap (cteCap (CTE x1 x2)) \<longrightarrow> capReplyMaster (cteCap (CTE x1 x2)) = capReplyMaster (cteCap (CTE c' n'))) \<and> isNotificationCap (cteCap (CTE x1 x2)) = isNotificationCap (cteCap (CTE c' n')) \<and> (isNotificationCap (cteCap (CTE x1 x2)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1 x2)) = capNtfnBadge (cteCap (CTE c' n'))) \<and> isEndpointCap (cteCap (CTE x1 x2)) = isEndpointCap (cteCap (CTE c' n')) \<and> (isEndpointCap (cteCap (CTE x1 x2)) \<longrightarrow> capEPBadge (cteCap (CTE x1 x2)) = capEPBadge (cteCap (CTE c' n'))) \<and> untypedRange (cteCap (CTE x1 x2)) = untypedRange (cteCap (CTE c' n')) \<and> capClass (cteCap (CTE x1 x2)) = capClass (cteCap (CTE c' n')) \<and> isZombie (cteCap (CTE x1 x2)) = isZombie (cteCap (CTE c' n')) \<and> isArchPageCap (cteCap (CTE x1 x2)) = isArchPageCap (cteCap (CTE c' n')) \<and> capBits (cteCap (CTE x1 x2)) = capBits (cteCap (CTE c' n')) \<and> global.capUntypedPtr (cteCap (CTE x1 x2)) = global.capUntypedPtr (cteCap (CTE c' n')) \<and> capRange (cteCap (CTE x1 x2)) = capRange (cteCap (CTE c' n')) \<and> isIRQControlCap (cteCap (CTE x1 x2)) = isIRQControlCap (cteCap (CTE c' n')) \<and> cteMDBNode (CTE x1 x2) = cteMDBNode (CTE c' n'); isUntypedCap (cteCap (CTE cap node)) = isUntypedCap (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> isNullCap (cteCap (CTE cap node)) = isNullCap (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> isReplyCap (cteCap (CTE cap node)) = isReplyCap (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> (isReplyCap (cteCap (CTE cap node)) \<longrightarrow> capReplyMaster (cteCap (CTE cap node)) = capReplyMaster (cteCap (?cte'43 p p' c n c' n' cap node x1 x2))) \<and> isNotificationCap (cteCap (CTE cap node)) = isNotificationCap (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> (isNotificationCap (cteCap (CTE cap node)) \<longrightarrow> capNtfnBadge (cteCap (CTE cap node)) = capNtfnBadge (cteCap (?cte'43 p p' c n c' n' cap node x1 x2))) \<and> isEndpointCap (cteCap (CTE cap node)) = isEndpointCap (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> (isEndpointCap (cteCap (CTE cap node)) \<longrightarrow> capEPBadge (cteCap (CTE cap node)) = capEPBadge (cteCap (?cte'43 p p' c n c' n' cap node x1 x2))) \<and> untypedRange (cteCap (CTE cap node)) = untypedRange (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> capClass (cteCap (CTE cap node)) = capClass (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> isZombie (cteCap (CTE cap node)) = isZombie (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> isArchPageCap (cteCap (CTE cap node)) = isArchPageCap (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> capBits (cteCap (CTE cap node)) = capBits (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> global.capUntypedPtr (cteCap (CTE cap node)) = global.capUntypedPtr (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> capRange (cteCap (CTE cap node)) = capRange (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> isIRQControlCap (cteCap (CTE cap node)) = isIRQControlCap (cteCap (?cte'43 p p' c n c' n' cap node x1 x2)) \<and> cteMDBNode (CTE cap node) = cteMDBNode (?cte'43 p p' c n c' n' cap node x1 x2)\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cap node x1 x2. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE cap node); m p' = Some (CTE x1 x2); isUntypedCap cap \<longrightarrow> isUntypedCap x1 \<longrightarrow> (untypedRange cap \<subseteq> untypedRange x1 \<or> untypedRange x1 \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange x1 = {}) \<and> (untypedRange cap \<subset> untypedRange x1 \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange cap \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange x1 \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'); isUntypedCap (cteCap (CTE x1 x2)) = isUntypedCap (cteCap (CTE c' n')) \<and> isNullCap (cteCap (CTE x1 x2)) = isNullCap (cteCap (CTE c' n')) \<and> isReplyCap (cteCap (CTE x1 x2)) = isReplyCap (cteCap (CTE c' n')) \<and> (isReplyCap (cteCap (CTE x1 x2)) \<longrightarrow> capReplyMaster (cteCap (CTE x1 x2)) = capReplyMaster (cteCap (CTE c' n'))) \<and> isNotificationCap (cteCap (CTE x1 x2)) = isNotificationCap (cteCap (CTE c' n')) \<and> (isNotificationCap (cteCap (CTE x1 x2)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1 x2)) = capNtfnBadge (cteCap (CTE c' n'))) \<and> isEndpointCap (cteCap (CTE x1 x2)) = isEndpointCap (cteCap (CTE c' n')) \<and> (isEndpointCap (cteCap (CTE x1 x2)) \<longrightarrow> capEPBadge (cteCap (CTE x1 x2)) = capEPBadge (cteCap (CTE c' n'))) \<and> untypedRange (cteCap (CTE x1 x2)) = untypedRange (cteCap (CTE c' n')) \<and> capClass (cteCap (CTE x1 x2)) = capClass (cteCap (CTE c' n')) \<and> isZombie (cteCap (CTE x1 x2)) = isZombie (cteCap (CTE c' n')) \<and> isArchPageCap (cteCap (CTE x1 x2)) = isArchPageCap (cteCap (CTE c' n')) \<and> capBits (cteCap (CTE x1 x2)) = capBits (cteCap (CTE c' n')) \<and> global.capUntypedPtr (cteCap (CTE x1 x2)) = global.capUntypedPtr (cteCap (CTE c' n')) \<and> capRange (cteCap (CTE x1 x2)) = capRange (cteCap (CTE c' n')) \<and> isIRQControlCap (cteCap (CTE x1 x2)) = isIRQControlCap (cteCap (CTE c' n')) \<and> cteMDBNode (CTE x1 x2) = cteMDBNode (CTE c' n'); isUntypedCap (cteCap (CTE cap node)) = isUntypedCap (cteCap (CTE c n)) \<and> isNullCap (cteCap (CTE cap node)) = isNullCap (cteCap (CTE c n)) \<and> isReplyCap (cteCap (CTE cap node)) = isReplyCap (cteCap (CTE c n)) \<and> (isReplyCap (cteCap (CTE cap node)) \<longrightarrow> capReplyMaster (cteCap (CTE cap node)) = capReplyMaster (cteCap (CTE c n))) \<and> isNotificationCap (cteCap (CTE cap node)) = isNotificationCap (cteCap (CTE c n)) \<and> (isNotificationCap (cteCap (CTE cap node)) \<longrightarrow> capNtfnBadge (cteCap (CTE cap node)) = capNtfnBadge (cteCap (CTE c n))) \<and> isEndpointCap (cteCap (CTE cap node)) = isEndpointCap (cteCap (CTE c n)) \<and> (isEndpointCap (cteCap (CTE cap node)) \<longrightarrow> capEPBadge (cteCap (CTE cap node)) = capEPBadge (cteCap (CTE c n))) \<and> untypedRange (cteCap (CTE cap node)) = untypedRange (cteCap (CTE c n)) \<and> capClass (cteCap (CTE cap node)) = capClass (cteCap (CTE c n)) \<and> isZombie (cteCap (CTE cap node)) = isZombie (cteCap (CTE c n)) \<and> isArchPageCap (cteCap (CTE cap node)) = isArchPageCap (cteCap (CTE c n)) \<and> capBits (cteCap (CTE cap node)) = capBits (cteCap (CTE c n)) \<and> global.capUntypedPtr (cteCap (CTE cap node)) = global.capUntypedPtr (cteCap (CTE c n)) \<and> capRange (cteCap (CTE cap node)) = capRange (cteCap (CTE c n)) \<and> isIRQControlCap (cteCap (CTE cap node)) = isIRQControlCap (cteCap (CTE c n)) \<and> cteMDBNode (CTE cap node) = cteMDBNode (CTE c n)\<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' \<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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE cap n); m p' = Some (CTE x1 n'); untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c\<rbrakk> \<Longrightarrow> (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') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange (cteCap (CTE c n)) \<subseteq> usableUntypedRange (cteCap (CTE cap n)); usableUntypedRange (cteCap (CTE c' n')) \<subseteq> usableUntypedRange (cteCap (CTE x1 n'))\<rbrakk> \<Longrightarrow> (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') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange (cteCap (CTE c n)) \<subseteq> usableUntypedRange (cteCap (CTE cap n)); usableUntypedRange (cteCap (CTE c' n')) \<subseteq> usableUntypedRange (cteCap (CTE x1 n')); \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m')\<rbrakk> \<Longrightarrow> (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')
 2. \<And>p p' c n c' n' cap x1 pa p'a. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange (cteCap (CTE c n)) \<subseteq> usableUntypedRange (cteCap (CTE cap n)); usableUntypedRange (cteCap (CTE c' n')) \<subseteq> usableUntypedRange (cteCap (CTE x1 n'))\<rbrakk> \<Longrightarrow> (p'a \<in> descendants_of' pa m) = (p'a \<in> descendants_of' pa m') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m')\<rbrakk> \<Longrightarrow> (untypedRange c \<subset> untypedRange c' \<longrightarrow> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> 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')
 2. \<And>p p' c n c' n' cap x1 pa p'a. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange (cteCap (CTE c n)) \<subseteq> usableUntypedRange (cteCap (CTE cap n)); usableUntypedRange (cteCap (CTE c' n')) \<subseteq> usableUntypedRange (cteCap (CTE x1 n'))\<rbrakk> \<Longrightarrow> (p'a \<in> descendants_of' pa m) = (p'a \<in> descendants_of' pa m') proof (prove)
goal (4 subgoals):
 1. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c \<subset> untypedRange c'\<rbrakk> \<Longrightarrow> untypedRange c \<inter> usableUntypedRange c' = {}
 2. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c' \<subset> untypedRange c\<rbrakk> \<Longrightarrow> untypedRange c' \<inter> usableUntypedRange c = {}
 3. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c = untypedRange c'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p'
 4. \<And>p p' c n c' n' cap x1 pa p'a. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange (cteCap (CTE c n)) \<subseteq> usableUntypedRange (cteCap (CTE cap n)); usableUntypedRange (cteCap (CTE c' n')) \<subseteq> usableUntypedRange (cteCap (CTE x1 n'))\<rbrakk> \<Longrightarrow> (p'a \<in> descendants_of' pa m) = (p'a \<in> descendants_of' pa m') proof (prove)
goal (4 subgoals):
 1. \<And>p p' c n c' n' cap x1 x. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; isUntypedCap x1; isUntypedCap cap; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> usableUntypedRange cap = {} \<or> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c \<subseteq> untypedRange c'; untypedRange c \<inter> usableUntypedRange c' \<noteq> {}; x \<in> untypedRange c'; p \<in> descendants_of' p' m'; untypedRange c \<inter> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c' \<subset> untypedRange c\<rbrakk> \<Longrightarrow> untypedRange c' \<inter> usableUntypedRange c = {}
 3. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m' \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m' \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c = untypedRange c'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {} \<or> p = p'
 4. \<And>p p' c n c' n' cap x1 pa p'a. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange (cteCap (CTE c n)) \<subseteq> usableUntypedRange (cteCap (CTE cap n)); usableUntypedRange (cteCap (CTE c' n')) \<subseteq> usableUntypedRange (cteCap (CTE x1 n'))\<rbrakk> \<Longrightarrow> (p'a \<in> descendants_of' pa m) = (p'a \<in> descendants_of' pa m') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; isUntypedCap x1; isUntypedCap cap; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); p' \<in> descendants_of' p m' \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m' \<and> usableUntypedRange x1 = {}; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c'; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c = untypedRange c'; p' \<in> descendants_of' p m' \<longrightarrow> usableUntypedRange c \<noteq> {}; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {}
 2. \<And>p p' c n c' n' cap x1 pa p'a. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange (cteCap (CTE c n)) \<subseteq> usableUntypedRange (cteCap (CTE cap n)); usableUntypedRange (cteCap (CTE c' n')) \<subseteq> usableUntypedRange (cteCap (CTE x1 n'))\<rbrakk> \<Longrightarrow> (p'a \<in> descendants_of' pa m) = (p'a \<in> descendants_of' pa m') proof (prove)
goal (3 subgoals):
 1. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; isUntypedCap x1; isUntypedCap cap; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c'; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c = untypedRange c'; p' \<in> descendants_of' p m' \<longrightarrow> usableUntypedRange c \<noteq> {}; p \<noteq> p'; p' \<in> descendants_of' p m' \<and> usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {}
 2. \<And>p p' c n c' n' cap x1. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; isUntypedCap x1; isUntypedCap cap; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c'; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1; \<And>p p'. (p' \<in> descendants_of' p m) = (p' \<in> descendants_of' p m'); untypedRange c = untypedRange c'; p' \<in> descendants_of' p m' \<longrightarrow> usableUntypedRange c \<noteq> {}; p \<noteq> p'; p \<in> descendants_of' p' m' \<and> usableUntypedRange x1 = {}\<rbrakk> \<Longrightarrow> p \<in> descendants_of' p' m' \<and> usableUntypedRange c' = {}
 3. \<And>p p' c n c' n' cap x1 pa p'a. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange (cteCap (CTE c n)) \<subseteq> usableUntypedRange (cteCap (CTE cap n)); usableUntypedRange (cteCap (CTE c' n')) \<subseteq> usableUntypedRange (cteCap (CTE x1 n'))\<rbrakk> \<Longrightarrow> (p'a \<in> descendants_of' pa m) = (p'a \<in> descendants_of' pa m') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cap x1 pa p'a. \<lbrakk>m' p' = Some (CTE c' n'); isUntypedCap c'; m' p = Some (CTE c n); isUntypedCap c; untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}; isUntypedCap x1; isUntypedCap cap; untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange x1 = {}; (x1 = capability.NullCap) = (c' = capability.NullCap); (cap = capability.NullCap) = (c = capability.NullCap); untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange cap = {}; untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange x1 = {} \<or> p = p'; isReplyCap x1 = isReplyCap c'; isReplyCap cap = isReplyCap c; isReplyCap c' \<longrightarrow> capReplyMaster x1 = capReplyMaster c'; isReplyCap c \<longrightarrow> capReplyMaster cap = capReplyMaster c; isNotificationCap x1 = isNotificationCap c'; isNotificationCap cap = isNotificationCap c; isNotificationCap c' \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c'; isNotificationCap c \<longrightarrow> capNtfnBadge cap = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c'; isEndpointCap cap = isEndpointCap c; isEndpointCap c' \<longrightarrow> capEPBadge x1 = capEPBadge c'; isEndpointCap c \<longrightarrow> capEPBadge cap = capEPBadge c; untypedRange x1 = untypedRange c'; untypedRange cap = untypedRange c; capClass x1 = capClass c'; capClass cap = capClass c; isZombie x1 = isZombie c'; isZombie cap = isZombie c; isArchPageCap x1 = isArchPageCap c'; isArchPageCap cap = isArchPageCap c; capBits x1 = capBits c'; capBits cap = capBits c; global.capUntypedPtr x1 = global.capUntypedPtr c'; global.capUntypedPtr cap = global.capUntypedPtr c; capRange x1 = capRange c'; isIRQControlCap x1 = isIRQControlCap c'; capRange cap = capRange c; isIRQControlCap cap = isIRQControlCap c; usableUntypedRange c \<subseteq> usableUntypedRange cap; usableUntypedRange c' \<subseteq> usableUntypedRange x1\<rbrakk> \<Longrightarrow> (p'a \<in> descendants_of' pa m) = (p'a \<in> descendants_of' pa m') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' cap x1 pa p'a. (p'a \<in> descendants_of' pa m) = (p'a \<in> descendants_of' pa m') proof (prove)
goal (1 subgoal):
 1. \<And>pa p'a. lfp (\<lambda>p x. m \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x)) p'a = lfp (\<lambda>p x. m' \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x)) p'a proof (prove)
goal (1 subgoal):
 1. \<And>pa p'a. (\<lambda>p x. m \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x)) = (\<lambda>p x. m' \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x)) proof (prove)
goal (2 subgoals):
 1. \<And>pa p'a. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> (\<lambda>p x. m \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x)) = (\<lambda>p x. m' \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x))
 2. \<And>pa p'a p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>pa p'a p x. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> (m \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x)) = (m' \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x))
 2. \<And>pa p'a p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>pa p x. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> (m' \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x)) = (m' \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x))
 2. \<And>pa p'a p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p' proof (prove)
goal (3 subgoals):
 1. \<And>pa p x. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m \<turnstile> pa parentOf x = m' \<turnstile> pa parentOf x\<rbrakk> \<Longrightarrow> (m' \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> pa parentOf x)) = (m' \<turnstile> pa \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x \<or> (\<exists>c'. p c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> pa parentOf x))
 2. \<And>pa p x. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> m \<turnstile> pa parentOf x = m' \<turnstile> pa parentOf x
 3. \<And>pa p'a p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>pa p x. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> m \<turnstile> pa parentOf x = m' \<turnstile> pa parentOf x
 2. \<And>pa p'a p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p' proof (prove)
goal (4 subgoals):
 1. \<And>pa p x xa cte cte'. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m xa = Some cte; m' xa = Some cte'\<rbrakk> \<Longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 2. \<And>pa p x xa cte cte'. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m xa = Some cte; m' xa = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> cteMDBNode cte = cteMDBNode cte'
 3. \<And>pa p x pb. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> mdb_next m pb = mdb_next m' pb
 4. \<And>pa p'a p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p' proof (prove)
goal:
No subgoals!