theory Untyped_AI

lemma create_cap_descendants_range[wp]:
 "\<lbrace>descendants_range c p and
   K (cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}) and
   cte_wp_at ((\<noteq>) cap.NullCap) p and
   cte_wp_at ((=) cap.NullCap) cref and
   valid_mdb\<rbrace>
  create_cap tp sz p dev (cref,oref)
  \<lbrace>\<lambda>rv. descendants_range c p\<rbrace>" apply (simp add: create_cap_def descendants_range_def cte_wp_at_caps_of_state set_cdt_def) apply (wp set_cap_caps_of_state2 | simp del: fun_upd_apply)+ apply (clarsimp simp: cte_wp_at_caps_of_state swp_def valid_mdb_def simp del: fun_upd_apply) apply (subst (asm) mdb_insert_abs.descendants_child) apply (rule mdb_insert_abs.intro) apply clarsimp apply (erule (1) mdb_cte_at_Null_None) apply (erule (1) mdb_cte_at_Null_descendants) apply clarsimp apply (rule conjI, clarsimp) apply blast apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>descendants_range c p and K (cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}) and cte_wp_at ((\<noteq>) NullCap) p and cte_wp_at ((=) NullCap) cref and valid_mdb\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. descendants_range c p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}) and (\<lambda>y. cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}) and cte_wp_at ((\<noteq>) NullCap) p and cte_wp_at ((=) NullCap) cref and valid_mdb\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := cdt(cref \<mapsto> p)\<rparr>)
od;
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}) \<and> cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {} \<and> cte_wp_at ((\<noteq>) NullCap) p s \<and> cte_wp_at ((=) NullCap) cref s \<and> valid_mdb s \<Longrightarrow> \<forall>p'\<in>descendants_of p ((cdt s)(cref \<mapsto> p)). \<exists>cap. ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev)) p' = Some cap \<and> cap_range cap \<inter> cap_range c = {} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> descendants_of p ((cdt s)(cref \<mapsto> p)); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev)) (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> mdb_insert_abs (cdt s) p cref
 2. \<And>s a b cap. \<lbrakk>(a, b) \<in> (if p \<in> descendants_of p (cdt s) \<or> p = p then descendants_of p (cdt s) \<union> {cref} else descendants_of p (cdt s)); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev)) (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {} proof (prove)
goal (4 subgoals):
 1. \<And>s a b cap. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> p \<noteq> cref
 2. \<And>s a b cap. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cdt s cref = None
 3. \<And>s a b cap. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_of cref (cdt s) = {}
 4. \<And>s a b cap. \<lbrakk>(a, b) \<in> (if p \<in> descendants_of p (cdt s) \<or> p = p then descendants_of p (cdt s) \<union> {cref} else descendants_of p (cdt s)); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev)) (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {} proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cdt s cref = None
 2. \<And>s a b cap. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_of cref (cdt s) = {}
 3. \<And>s a b cap. \<lbrakk>(a, b) \<in> (if p \<in> descendants_of p (cdt s) \<or> p = p then descendants_of p (cdt s) \<union> {cref} else descendants_of p (cdt s)); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev)) (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_of cref (cdt s) = {}
 2. \<And>s a b cap. \<lbrakk>(a, b) \<in> (if p \<in> descendants_of p (cdt s) \<or> p = p then descendants_of p (cdt s) \<union> {cref} else descendants_of p (cdt s)); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev)) (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> (if p \<in> descendants_of p (cdt s) \<or> p = p then descendants_of p (cdt s) \<union> {cref} else descendants_of p (cdt s)); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev)) (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) = cref \<or> (a, b) \<in> descendants_of p (cdt s); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> ((a, b) = cref \<longrightarrow> cap_range (default_cap tp oref sz dev) \<inter> cap_range c = {}) \<and> ((a, b) \<noteq> cref \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {})) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s (a, b) = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cref = (a, b)\<rbrakk> \<Longrightarrow> cap_range (default_cap tp oref sz dev) \<inter> cap_range c = {}
 2. \<And>s a b cap. \<lbrakk>(a, b) = cref \<or> (a, b) \<in> descendants_of p (cdt s); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> (a, b) \<noteq> cref \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) = cref \<or> (a, b) \<in> descendants_of p (cdt s); \<forall>p'\<in>descendants_of p (cdt s). \<exists>cap. caps_of_state s p' = Some cap \<and> cap_range cap \<inter> cap_range c = {}; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; caps_of_state s cref = Some NullCap; caps_of_state s p = Some cap; NullCap \<noteq> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> (a, b) \<noteq> cref \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap_range cap \<inter> cap_range c = {}) proof (prove)
goal:
No subgoals!