theory CSpace_AI

lemma (in mdb_insert_abs) reply_masters_mdb_simple:
  assumes u: "reply_masters_mdb m cs"
  assumes src: "cs src = Some c"
  assumes sr: "\<not>is_reply_cap c \<and> \<not>is_master_reply_cap c"
  assumes nr: "\<not>is_reply_cap cap \<and> \<not>is_master_reply_cap cap"
  shows "reply_masters_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" unfolding reply_masters_mdb_def using u src sr nr apply (intro allI impI) apply (simp add: descendants_child del: split_paired_Ex) apply (case_tac "ptr = dest", simp add: is_cap_simps) apply (simp del: split_paired_Ex) apply (unfold reply_masters_mdb_def) apply (elim allE) apply (erule(1) impE) apply (elim conjE, simp add: neq is_cap_simps) apply (intro conjI impI) apply fastforce apply (rule ccontr, simp) apply (rule ballI, rule ccontr, simp add: descendants_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t True rights) \<longrightarrow> (m(dest \<mapsto> src)) ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr (m(dest \<mapsto> src)). \<exists>rights'. (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
using this:
reply_masters_mdb m cs
cs src = Some c
\<not> is_reply_cap c \<and> \<not> is_master_reply_cap c
\<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap

goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t True rights) \<longrightarrow> (m(dest \<mapsto> src)) ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr (m(dest \<mapsto> src)). \<exists>rights'. (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; cs src = Some c; \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c; \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap; (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (m(dest \<mapsto> src)) ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr (m(dest \<mapsto> src)). \<exists>rights'. (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; cs src = Some c; \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c; \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap; (if ptr = dest then Some cap else cs ptr) = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src = dest \<longrightarrow> ptr \<noteq> dest \<and> (ptr \<noteq> dest \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) \<and> (src \<noteq> dest \<longrightarrow> ptr \<noteq> dest \<and> (ptr \<noteq> dest \<longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (ptr = src \<longrightarrow> m src = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; cs src = Some c; \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c; \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap; (if ptr = dest then Some cap else cs ptr) = Some (ReplyCap t True rights); ptr \<noteq> dest\<rbrakk> \<Longrightarrow> (src = dest \<longrightarrow> ptr \<noteq> dest \<and> (ptr \<noteq> dest \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) \<and> (src \<noteq> dest \<longrightarrow> ptr \<noteq> dest \<and> (ptr \<noteq> dest \<longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (ptr = src \<longrightarrow> m src = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; cs src = Some c; \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c; \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest\<rbrakk> \<Longrightarrow> (src = dest \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<noteq> dest \<longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (ptr = src \<longrightarrow> m src = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); cs src = Some c; \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c; \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest\<rbrakk> \<Longrightarrow> (src = dest \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<noteq> dest \<longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (ptr = src \<longrightarrow> m src = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some c; \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c; \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; cs (?ptr57 ptr t rights) = Some (ReplyCap (?t58 ptr t rights) True (?rights59 ptr t rights)) \<longrightarrow> m (?ptr57 ptr t rights) = None \<and> (\<forall>ptr'\<in>descendants_of (?ptr57 ptr t rights) m. \<exists>rights'. cs ptr' = Some (ReplyCap (?t58 ptr t rights) False rights'))\<rbrakk> \<Longrightarrow> (src = dest \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<noteq> dest \<longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (ptr = src \<longrightarrow> m src = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some c; \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c; \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> (src = dest \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<noteq> dest \<longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (ptr = src \<longrightarrow> m src = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some c; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; \<forall>x R. c \<noteq> ReplyCap x False R; \<forall>x R. c \<noteq> ReplyCap x True R; \<forall>x R. cap \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<and> (src \<notin> descendants_of ptr m \<and> ptr \<noteq> src \<longrightarrow> (\<forall>ptr'\<in>descendants_of ptr m. ptr' \<noteq> dest)) proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some c; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; \<forall>x R. c \<noteq> ReplyCap x False R; \<forall>x R. c \<noteq> ReplyCap x True R; \<forall>x R. cap \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m
 2. \<And>ptr t rights. \<lbrakk>cs src = Some c; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; \<forall>x R. c \<noteq> ReplyCap x False R; \<forall>x R. c \<noteq> ReplyCap x True R; \<forall>x R. cap \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> ptr \<noteq> src
 3. \<And>ptr t rights. \<lbrakk>cs src = Some c; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; \<forall>x R. c \<noteq> ReplyCap x False R; \<forall>x R. c \<noteq> ReplyCap x True R; \<forall>x R. cap \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); src \<notin> descendants_of ptr m \<and> ptr \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of ptr m. ptr' \<noteq> dest proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some c; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; \<forall>x R. c \<noteq> ReplyCap x False R; \<forall>x R. c \<noteq> ReplyCap x True R; \<forall>x R. cap \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> ptr \<noteq> src
 2. \<And>ptr t rights. \<lbrakk>cs src = Some c; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; \<forall>x R. c \<noteq> ReplyCap x False R; \<forall>x R. c \<noteq> ReplyCap x True R; \<forall>x R. cap \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); src \<notin> descendants_of ptr m \<and> ptr \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of ptr m. ptr' \<noteq> dest proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some c; cs ptr = Some (ReplyCap t True rights); ptr \<noteq> dest; \<forall>x R. c \<noteq> ReplyCap x False R; \<forall>x R. c \<noteq> ReplyCap x True R; \<forall>x R. cap \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); src \<notin> descendants_of ptr m \<and> ptr \<noteq> src\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of ptr m. ptr' \<noteq> dest proof (prove)
goal:
No subgoals!