theory CNodeInv_AI

lemma reply_caps_mdb_n:
  "reply_caps_mdb n cs'" proof - from valid_mdb have "reply_caps_mdb m cs" by (simp add: cs_def m valid_mdb_def2 reply_mdb_def) thus ?thesis using cap cap' unfolding reply_caps_mdb_def cs'_def n_def n'_def apply (intro allI impI) apply (simp split: if_split_asm del: split_paired_All split_paired_Ex) apply (elim allE) apply (drule weak_derived_Reply_eq(1) [OF sder], simp del: split_paired_Ex) apply (erule impE, fastforce) apply (intro conjI impI) apply (clarsimp elim!: weak_derived_Reply_eq(2) [OF dder]) apply (erule exEI, clarsimp) apply (elim allE) apply (drule weak_derived_Reply_eq(1) [OF dder], simp del: split_paired_Ex) apply (erule impE, fastforce) apply (intro conjI impI) apply (clarsimp elim!: weak_derived_Reply_eq(2) [OF sder]) apply (erule exEI, clarsimp) apply (erule_tac x=ptr in allE, erule_tac x=t in allE) apply (erule impE, fastforce) apply (intro conjI impI) apply (clarsimp elim!: weak_derived_Reply_eq(2) [OF dder]) apply (clarsimp elim!: weak_derived_Reply_eq(2) [OF sder]) apply fastforce done qed

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

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

goal (1 subgoal):
 1. reply_caps_mdb n cs' proof (prove)
using this:
reply_caps_mdb m cs

goal (1 subgoal):
 1. reply_caps_mdb n cs' proof (prove)
using this:
reply_caps_mdb m cs
cs src = Some cap
cs dest = Some cap'

goal (1 subgoal):
 1. reply_caps_mdb n cs' proof (prove)
using this:
\<forall>ptr t rights. cs ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. m ptr = Some ptr' \<and> cs ptr' = Some (ReplyCap t True rights'))
cs src = Some cap
cs dest = Some cap'

goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. ((\<lambda>n. if m n = Some src then Some dest else if m n = Some dest then Some src else m n)(src := if m dest = Some src then Some dest else if m dest = Some dest then Some src else m dest, dest := if m src = Some src then Some dest else if m src = Some dest then Some src else m src)) ptr = Some ptr' \<and> (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr' = Some (ReplyCap t True rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. m ptr = Some ptr' \<and> cs ptr' = Some (ReplyCap t True rights')); cs src = Some cap; cs dest = Some cap'; (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr' rights'. ((\<lambda>n. if m n = Some src then Some dest else if m n = Some dest then Some src else m n)(src := if m dest = Some src then Some dest else if m dest = Some dest then Some src else m dest, dest := if m src = Some src then Some dest else if m src = Some dest then Some src else m src)) ptr = Some ptr' \<and> (cs(src \<mapsto> dcap, dest \<mapsto> scap)) ptr' = Some (ReplyCap t True rights') proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr = dest; scap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> (m src = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m src \<noteq> Some dest \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr = src; dcap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 3. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; scap = ReplyCap t False rights; (\<exists>rightsa. cs (?ptr278 ptr t rights) = Some (ReplyCap (?t279 ptr t rights) False rightsa)) \<longrightarrow> (\<exists>ptr'. m (?ptr278 ptr t rights) = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap (?t279 ptr t rights) True rights')))\<rbrakk> \<Longrightarrow> (m src = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m src \<noteq> Some dest \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr = src; dcap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 3. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; (\<exists>rightsa. cs (?ptr278 dest t rights) = Some (ReplyCap (?t279 dest t rights) False rightsa)) \<longrightarrow> (\<exists>ptr'. m (?ptr278 dest t rights) = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap (?t279 dest t rights) True rights'))); \<exists>R'. cap = ReplyCap t False R'\<rbrakk> \<Longrightarrow> (m src = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m src \<noteq> Some dest \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr = src; dcap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 3. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t False R'; \<exists>ptr'. m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))\<rbrakk> \<Longrightarrow> (m src = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m src \<noteq> Some dest \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr = src; dcap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 3. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (4 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t False R'; \<exists>ptr'. m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m src = Some dest\<rbrakk> \<Longrightarrow> \<exists>rights'. dcap = ReplyCap t True rights'
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t False R'; \<exists>ptr'. m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m src \<noteq> Some dest\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))
 3. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr = src; dcap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 4. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = dest; \<exists>R'. cap = ReplyCap t False R'; \<exists>ptr'. m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m src \<noteq> Some dest\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m src = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr = src; dcap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 3. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr = src; dcap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; dcap = ReplyCap t False rights; (\<exists>rightsa. cs (?ptr328 ptr t rights) = Some (ReplyCap (?t329 ptr t rights) False rightsa)) \<longrightarrow> (\<exists>ptr'. m (?ptr328 ptr t rights) = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap (?t329 ptr t rights) True rights')))\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; (\<exists>rightsa. cs (?ptr328 src t rights) = Some (ReplyCap (?t329 src t rights) False rightsa)) \<longrightarrow> (\<exists>ptr'. m (?ptr328 src t rights) = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap (?t329 src t rights) True rights'))); \<exists>R'. cap' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t False R'; \<exists>ptr'. m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m dest \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t False R'; \<exists>ptr'. m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m dest = Some src\<rbrakk> \<Longrightarrow> \<exists>rights'. scap = ReplyCap t True rights'
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t False R'; \<exists>ptr'. m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m dest \<noteq> Some src\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))
 3. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr = src; \<exists>R'. cap' = ReplyCap t False R'; \<exists>ptr'. m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m dest \<noteq> Some src\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))); cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True 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 False rights); (\<exists>rights. cs ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')))\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True 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 False rights); \<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))\<rbrakk> \<Longrightarrow> (m ptr = Some dest \<longrightarrow> (\<exists>rights'. dcap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some dest \<longrightarrow> (m ptr = Some src \<longrightarrow> (\<exists>rights'. scap = ReplyCap t True rights')) \<and> (m ptr \<noteq> Some src \<longrightarrow> (\<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))))))) proof (prove)
goal (3 subgoals):
 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 False rights); \<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m ptr = Some dest\<rbrakk> \<Longrightarrow> \<exists>rights'. dcap = ReplyCap t True rights'
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights); \<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m ptr \<noteq> Some dest; m ptr = Some src\<rbrakk> \<Longrightarrow> \<exists>rights'. scap = ReplyCap t True rights'
 3. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights); \<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m ptr \<noteq> Some dest; m ptr \<noteq> Some src\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')))) proof (prove)
goal (2 subgoals):
 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 False rights); \<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m ptr \<noteq> Some dest; m ptr = Some src\<rbrakk> \<Longrightarrow> \<exists>rights'. scap = ReplyCap t True rights'
 2. \<And>ptr t rights. \<lbrakk>cs src = Some cap; cs dest = Some cap'; ptr \<noteq> dest; ptr \<noteq> src; cs ptr = Some (ReplyCap t False rights); \<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m ptr \<noteq> Some dest; m ptr \<noteq> Some src\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True 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 False rights); \<exists>ptr'. m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')); m ptr \<noteq> Some dest; m ptr \<noteq> Some src\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')))) proof (prove)
goal:
No subgoals! proof (state)
this:
reply_caps_mdb n cs'

goal:
No subgoals!