theory CSpace_I

lemma untyped_mdb_init:
  "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte;
     caps_no_overlap' m (capRange cap); untyped_mdb' m;
     valid_objs' s; s \<turnstile>' cap;
     m = ctes_of s\<rbrakk>
    \<Longrightarrow> untyped_mdb' (m(p \<mapsto> CTE cap initMDBNode))" apply (clarsimp simp add: untyped_mdb'_def) apply (rule conjI) apply clarsimp apply (simp add: caps_no_overlap'_def) apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI) apply (drule (1) ctes_of_valid_cap')+ apply (drule valid_capAligned)+ apply (drule untypedCapRange)+ apply simp apply (cases cte) apply (rename_tac capability mdbnode) apply clarsimp apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode") prefer 2 apply (simp add: vmdb_def mdb_ptr_def mdb_ptr_axioms_def) apply (clarsimp simp: mdb_ptr.descendants_of_init') apply (simp add: caps_no_overlap'_def) apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI) apply (drule (1) ctes_of_valid_cap')+ apply (drule valid_capAligned untypedCapRange)+ apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb_ctes m; m p = Some cte; no_mdb cte; caps_no_overlap' m (capRange cap); untyped_mdb' m; valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> untyped_mdb' (m(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> (pa = p \<longrightarrow> isUntypedCap cap \<longrightarrow> (\<forall>p'. p' \<noteq> p \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange cap \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))))) \<and> (pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))))))) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa = p \<longrightarrow> isUntypedCap cap \<longrightarrow> (\<forall>p'. p' \<noteq> p \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange cap \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))))
 2. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; isUntypedCap cap; p' \<noteq> p; ctes_of s p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; \<forall>p c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange cap = {}; \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; isUntypedCap cap; p' \<noteq> p; ctes_of s p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; isUntypedCap cap; p' \<noteq> p; ctes_of s p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}; capRange c' \<inter> capRange cap = {}\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; isUntypedCap cap; p' \<noteq> p; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}; capRange c' \<inter> capRange cap = {}; valid_cap' c' s\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; m = ctes_of s; isUntypedCap cap; p' \<noteq> p; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}; capRange c' \<inter> capRange cap = {}; capAligned cap; capAligned c'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; m = ctes_of s; p' \<noteq> p; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}; capRange c' \<inter> capRange cap = {}; capAligned cap; capAligned c'; capRange cap = untypedRange cap\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (1 subgoal):
 1. \<And>pa x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode p'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p\<rbrakk> \<Longrightarrow> (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))))) proof (prove)
goal (2 subgoals):
 1. \<And>pa capability mdbnode p'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode\<rbrakk> \<Longrightarrow> (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))))
 2. \<And>pa capability mdbnode p'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) p capability mdbnode proof (prove)
goal (2 subgoals):
 1. \<And>pa capability mdbnode p'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) p capability mdbnode
 2. \<And>pa capability mdbnode p'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode\<rbrakk> \<Longrightarrow> (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))))) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode p'. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode\<rbrakk> \<Longrightarrow> (p' = p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)))) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. ctes_of s pa = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' pa ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))))) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode c n. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); caps_no_overlap' (ctes_of s) (capRange cap); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode; ctes_of s pa = Some (CTE c n); isUntypedCap c; \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p \<in> descendants_of' pa (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode c n. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); \<forall>p c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange cap = {}; \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode; ctes_of s pa = Some (CTE c n); isUntypedCap c; \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p \<in> descendants_of' pa (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode c n. \<lbrakk>valid_mdb_ctes (ctes_of s); ctes_of s p = Some (CTE capability mdbnode); no_mdb (CTE capability mdbnode); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode; ctes_of s pa = Some (CTE c n); isUntypedCap c; \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}; capRange c \<inter> capRange cap = {}\<rbrakk> \<Longrightarrow> p \<in> descendants_of' pa (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode c n. \<lbrakk>valid_mdb_ctes (ctes_of s); no_mdb (CTE capability mdbnode); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; valid_cap' cap s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode; isUntypedCap c; \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}; capRange c \<inter> capRange cap = {}; valid_cap' capability s; valid_cap' c s\<rbrakk> \<Longrightarrow> p \<in> descendants_of' pa (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode c n. \<lbrakk>valid_mdb_ctes (ctes_of s); no_mdb (CTE capability mdbnode); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode; \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}; capRange c \<inter> capRange cap = {}; capAligned cap; capAligned capability; capAligned c; capRange c = untypedRange c\<rbrakk> \<Longrightarrow> p \<in> descendants_of' pa (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>pa capability mdbnode c. \<lbrakk>valid_mdb_ctes (ctes_of s); no_mdb (CTE capability mdbnode); \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p (ctes_of s)); valid_objs' s; m = ctes_of s; cte = CTE capability mdbnode; pa \<noteq> p; mdb_ptr (ctes_of s) p capability mdbnode; \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}; untypedRange c \<inter> capRange cap = {}; capAligned cap; capAligned capability; capAligned c; capRange c = untypedRange c\<rbrakk> \<Longrightarrow> p \<in> descendants_of' pa (ctes_of s) proof (prove)
goal:
No subgoals!