theory CNodeInv_AI

lemma reply_masters_mdb_n:
  "reply_masters_mdb n cs'" proof - from valid_mdb have r: "reply_masters_mdb m cs" by (simp add: cs_def m valid_mdb_def2 reply_mdb_def) have n_None:
    "\<And>t R. scap = cap.ReplyCap t True R \<Longrightarrow> n dest = None"
    "\<And>t R. dcap = cap.ReplyCap t True R \<Longrightarrow> n src = None" using r cap cap' unfolding reply_masters_mdb_def n_def by (drule_tac weak_derived_Reply_eq(1) [OF sder]
                   weak_derived_Reply_eq(1) [OF dder],
         fastforce simp: n'_def simp del: split_paired_All)+ show ?thesis unfolding reply_masters_mdb_def cs'_def using cap cap' r apply (intro allI impI) apply (simp add: n_None descendants s_d_swap_def
        split: if_split_asm del: split_paired_All) apply (unfold reply_masters_mdb_def)[1] apply (drule weak_derived_Reply_eq(1) [OF sder], simp del: split_paired_All) apply (elim allE, erule impE, fastforce, elim conjE) apply (intro impI conjI) apply (drule(1) bspec) apply clarsimp apply (rule weak_derived_Reply_eq(2) [OF dder]) apply simp apply fastforce apply fastforce apply (unfold reply_masters_mdb_def)[1] apply (drule weak_derived_Reply_eq(1) [OF dder], simp del: split_paired_All) apply (elim allE, erule impE, fastforce, elim conjE) apply (intro impI conjI) apply (drule(1) bspec, clarsimp, rule weak_derived_Reply_eq(2) [OF sder], simp) apply fastforce+ apply (unfold reply_masters_mdb_def)[1] apply (erule_tac x=ptr in allE, erule_tac x=t in allE) apply (elim allE impE, fastforce) apply (erule conjE, simp add: n_def n'_def) apply (fastforce intro:weak_derived_Reply_eq(2)[OF dder] weak_derived_Reply_eq(2)[OF sder])+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_mdb n cs' proof (state)
goal (1 subgoal):
 1. reply_masters_mdb n cs' proof (chain)
picking this:
valid_mdb s proof (prove)
using this:
valid_mdb s

goal (1 subgoal):
 1. reply_masters_mdb m cs proof (state)
this:
reply_masters_mdb m cs

goal (1 subgoal):
 1. reply_masters_mdb n cs' proof (prove)
goal (1 subgoal):
 1. (\<And>t R. scap = ReplyCap t True R \<Longrightarrow> n dest = None) &&& (\<And>t R. dcap = ReplyCap t True R \<Longrightarrow> n src = None) proof (prove)
using this:
reply_masters_mdb m cs
cs src = Some cap
cs dest = Some cap'

goal (1 subgoal):
 1. (\<And>t R. scap = ReplyCap t True R \<Longrightarrow> n dest = None) &&& (\<And>t R. dcap = ReplyCap t True R \<Longrightarrow> n src = None) proof (prove)
using this:
\<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 cap
cs dest = Some cap'

goal (1 subgoal):
 1. (\<And>t R. scap = ReplyCap t True R \<Longrightarrow> (n'(src := n' dest, dest := n' src)) dest = None) &&& (\<And>t R. dcap = ReplyCap t True R \<Longrightarrow> (n'(src := n' dest, dest := n' src)) src = None) proof (state)
this:
scap = ReplyCap ?t True ?R \<Longrightarrow> n dest = None
dcap = ReplyCap ?t True ?R \<Longrightarrow> n src = None

goal (1 subgoal):
 1. reply_masters_mdb n cs' proof (prove)
goal (1 subgoal):
 1. reply_masters_mdb n cs' proof (prove)
goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr = Some (ReplyCap t True rights) \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr n. \<exists>rights'. (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
using this:
cs src = Some cap
cs dest = Some cap'
reply_masters_mdb m cs

goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr = Some (ReplyCap t True rights) \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr n. \<exists>rights'. (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr n. \<exists>rights'. (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = dest; scap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (dest \<in> descendants_of src m \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of src m \<longrightarrow> (\<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 3. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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>cs src = Some cap; cs dest = Some cap'; \<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')); ptr = dest; scap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (dest \<in> descendants_of src m \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of src m \<longrightarrow> (\<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 3. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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. \<lbrakk>cs src = Some cap; cs dest = Some cap'; \<forall>ptr t. (\<exists>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')); ptr = dest; \<exists>R'. cap = ReplyCap t True R'\<rbrakk> \<Longrightarrow> (dest \<in> descendants_of src m \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of src m \<longrightarrow> (\<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 3. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> (dest \<in> descendants_of src m \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of src m \<longrightarrow> (\<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 3. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (5 subgoals):
 1. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<in> descendants_of src m\<rbrakk> \<Longrightarrow> \<exists>rights'. dcap = ReplyCap t False rights'
 2. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<in> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))
 3. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<notin> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 4. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 5. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (5 subgoals):
 1. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; dest \<in> descendants_of src m; \<exists>rights'. cs dest = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> \<exists>rights'. dcap = ReplyCap t False rights'
 2. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<in> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))
 3. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<notin> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 4. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 5. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (5 subgoals):
 1. \<And>a b t R' rights'. \<lbrakk>cs src = Some (ReplyCap t True R'); cs (a, b) = Some (ReplyCap t False rights'); m src = None; (a, b) \<in> descendants_of src m; dest = (a, b); cap = ReplyCap t True R'; cap' = ReplyCap t False rights'\<rbrakk> \<Longrightarrow> \<exists>rights'. dcap = ReplyCap t False rights'
 2. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<in> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))
 3. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<notin> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 4. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 5. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (5 subgoals):
 1. \<And>a b t R' rights'. \<lbrakk>cs src = Some (ReplyCap t True R'); cs (a, b) = Some (ReplyCap t False rights'); m src = None; (a, b) \<in> descendants_of src m; dest = (a, b); cap = ReplyCap t True R'; cap' = ReplyCap t False rights'\<rbrakk> \<Longrightarrow> cap' = ReplyCap t False (?R198 a b t R' rights')
 2. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<in> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))
 3. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<notin> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 4. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 5. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (4 subgoals):
 1. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<in> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))
 2. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<notin> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 3. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 4. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t True R'; m src = None; \<forall>ptr'\<in>descendants_of src m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); dest \<notin> descendants_of src m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of src m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 3. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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>cs src = Some cap; cs dest = Some cap'; \<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')); ptr = src; dcap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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. \<lbrakk>cs src = Some cap; cs dest = Some cap'; \<forall>ptr t. (\<exists>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')); ptr = src; \<exists>R'. cap' = ReplyCap t True R'\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t True R'; m dest = None; \<forall>ptr'\<in>descendants_of dest m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> (src \<in> descendants_of dest m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (src \<notin> descendants_of dest m \<longrightarrow> (\<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (4 subgoals):
 1. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t True R'; m dest = None; \<forall>ptr'\<in>descendants_of dest m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); src \<in> descendants_of dest m\<rbrakk> \<Longrightarrow> \<exists>rights'. scap = ReplyCap t False rights'
 2. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t True R'; m dest = None; \<forall>ptr'\<in>descendants_of dest m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); src \<in> descendants_of dest m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')
 3. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t True R'; m dest = None; \<forall>ptr'\<in>descendants_of dest m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); src \<notin> descendants_of dest m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 4. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t True R'; m dest = None; \<forall>ptr'\<in>descendants_of dest m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); src \<in> descendants_of dest m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of dest m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')
 2. \<And>ptr t. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t True R'; m dest = None; \<forall>ptr'\<in>descendants_of dest m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); src \<notin> descendants_of dest m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of dest m. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 3. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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 cap; cs dest = Some cap'; reply_masters_mdb m cs; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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 cap; cs dest = Some cap'; \<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')); ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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 cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights); \<forall>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'))\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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 cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; 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> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. scap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src, dest}. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {dest}. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> (ptr' = dest \<longrightarrow> (\<exists>rights'. scap = 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 cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t True rights); m ptr = None; \<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> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights') \<and> (\<exists>rights'. scap = ReplyCap t False rights')) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights'))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (dest \<notin> descendants_of ptr m \<longrightarrow> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = src \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t False rights')) \<and> (ptr' \<noteq> src \<longrightarrow> ptr' = dest \<longrightarrow> (\<exists>rights'. scap = ReplyCap t False rights'))))) proof (prove)
goal:
No subgoals! proof (state)
this:
reply_masters_mdb n cs'

goal:
No subgoals!