theory CSpace_AI

lemma (in mdb_insert_abs) reply_masters_mdb:
  assumes r: "reply_masters_mdb m cs"
  assumes src: "cs src = Some c"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes d: "is_derived m src cap c"
  shows "reply_masters_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" unfolding reply_masters_mdb_def using r d apply (intro allI impI) apply (simp add: descendants_child) apply (simp add: neq desc split: if_split_asm) apply (clarsimp simp: src is_derived_def is_cap_simps cap_master_cap_def) apply (unfold reply_masters_mdb_def) apply (intro conjI) apply (erule allE)+ apply (erule(1) impE) apply simp apply (rule impI) apply (erule conjE) apply (drule_tac x=src in bspec, assumption) apply (clarsimp simp: src is_derived_def is_cap_simps) apply (erule allE)+ apply (erule(1) impE) apply (rule impI, simp) apply (clarsimp simp: src is_derived_def is_cap_simps cap_master_cap_def) apply (erule allE)+ apply (erule(1) impE) apply (rule impI, simp, rule impI) apply (erule conjE) apply (drule_tac x=dest in bspec, assumption) apply (simp add: dst) 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
is_derived m src cap c

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; is_derived m src cap c; (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; is_derived m src cap c; (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 (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; is_derived m src (ReplyCap t True rights) c; ptr = dest; cap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<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; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<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 (3 subgoals):
 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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<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'))))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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'))))
 3. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); cs (?ptr69 ptr t rights) = Some (ReplyCap (?t71 ptr t rights) True (?rights73 ptr t rights)) \<longrightarrow> m (?ptr69 ptr t rights) = None \<and> (\<forall>ptr'\<in>descendants_of (?ptr69 ptr t rights) m. \<exists>rights'. cs ptr' = Some (ReplyCap (?t71 ptr t rights) False rights'))\<rbrakk> \<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'))))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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'))))
 3. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<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'))))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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'))))
 3. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> src \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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'))))
 3. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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'))))
 3. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<in> descendants_of ptr m; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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'))))
 3. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<in> descendants_of ptr m; m ptr = None; \<exists>rights'. cs src = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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'))))
 3. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (2 subgoals):
 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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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'))))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); cs (?ptr84 ptr t rights) = Some (ReplyCap (?t86 ptr t rights) True (?rights88 ptr t rights)) \<longrightarrow> m (?ptr84 ptr t rights) = None \<and> (\<forall>ptr'\<in>descendants_of (?ptr84 ptr t rights) m. \<exists>rights'. cs ptr' = Some (ReplyCap (?t86 ptr t rights) False rights'))\<rbrakk> \<Longrightarrow> 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'))))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> 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'))))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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 (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; src \<noteq> dest; cs src = Some (ReplyCap t True rights); m src = None \<and> (\<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); ptr = src\<rbrakk> \<Longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of src m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> 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>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); cs (?ptr110 ptr t rights) = Some (ReplyCap (?t112 ptr t rights) True (?rights114 ptr t rights)) \<longrightarrow> m (?ptr110 ptr t rights) = None \<and> (\<forall>ptr'\<in>descendants_of (?ptr110 ptr t rights) m. \<exists>rights'. cs ptr' = Some (ReplyCap (?t112 ptr t rights) False rights'))\<rbrakk> \<Longrightarrow> 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>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<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 \<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>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<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; dest \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> \<exists>rights'. cap = ReplyCap t False rights' proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<notin> descendants_of ptr m \<and> ptr \<noteq> src; dest \<in> descendants_of ptr m; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> \<exists>rights'. cap = ReplyCap t False rights' proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<notin> descendants_of ptr m \<and> ptr \<noteq> src; dest \<in> descendants_of ptr m; m ptr = None; \<exists>rights'. cs dest = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> \<exists>rights'. cap = ReplyCap t False rights' proof (prove)
goal:
No subgoals!