theory Fastpath_Equiv

lemma emptySlot_replymaster_rewrite[OF refl]:
  "mdbn = cteMDBNode cte \<Longrightarrow>
   monadic_rewrite True False
     ((\<lambda>_. mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0)
           and ((\<lambda>_. cteCap cte \<noteq> NullCap)
           and (cte_wp_at' ((=) cte) slot
           and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot
           and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte))
                    (mdbPrev mdbn)
           and (\<lambda>s. reply_masters_rvk_fb (ctes_of s))
           and (\<lambda>s. no_0 (ctes_of s)))))
     (emptySlot slot NullCap)
     (do updateMDB (mdbPrev mdbn) (mdbNext_update (K 0) o mdbFirstBadged_update (K True)
                                              o mdbRevocable_update (K True));
         setCTE slot makeObject
      od)" supply if_split[split del] apply (rule monadic_rewrite_gen_asm)+ apply (rule monadic_rewrite_guard_imp) apply (rule_tac P="slot \<noteq> 0" in monadic_rewrite_gen_asm) apply (clarsimp simp: emptySlot_def setCTE_updateCapMDB) apply (monadic_rewrite_l clearUntypedFreeIndex_simple_rewrite, simp) apply (monadic_rewrite_symb_exec_l_known cte) apply (simp add: updateMDB_def Let_def bind_assoc makeObject_cte case_Null_If) apply (rule monadic_rewrite_bind_tail) apply (rule monadic_rewrite_bind) apply (rule_tac P="mdbFirstBadged (cteMDBNode ctea) \<and> mdbRevocable (cteMDBNode ctea)"
                in monadic_rewrite_gen_asm) apply (rule monadic_rewrite_is_refl) apply (case_tac ctea, rename_tac mdbnode, case_tac mdbnode) apply simp apply (simp add: Retype_H.postCapDeletion_def) apply (rule monadic_rewrite_refl) apply (solves wp | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of reply_masters_rvk_fb_def) apply (fastforce simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbn = cteMDBNode cte \<Longrightarrow> monadic_rewrite True False ((\<lambda>_. mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0) and ((\<lambda>_. cteCap cte \<noteq> capability.NullCap) and (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))))) (emptySlot slot capability.NullCap) (do updateMDB (mdbPrev mdbn) (mdbNext_update (K 0) \<circ> mdbFirstBadged_update (K True) \<circ> mdbRevocable_update (K True));
setCTE slot makeObject
od) proof (prove)
goal (1 subgoal):
 1. mdbn = cteMDBNode cte \<Longrightarrow> monadic_rewrite True False ((\<lambda>_. mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0) and ((\<lambda>_. cteCap cte \<noteq> capability.NullCap) and (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))))) (emptySlot slot capability.NullCap) (do updateMDB (mdbPrev mdbn) (mdbNext_update (K 0) \<circ> mdbFirstBadged_update (K True) \<circ> mdbRevocable_update (K True));
setCTE slot makeObject
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> monadic_rewrite True False (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) (emptySlot slot capability.NullCap) (do updateMDB (mdbPrev mdbn) (mdbNext_update (K 0) \<circ> mdbFirstBadged_update (K True) \<circ> mdbRevocable_update (K True));
setCTE slot makeObject
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q4 (emptySlot slot capability.NullCap) (do updateMDB (mdbPrev mdbn) (mdbNext_update (K 0) \<circ> mdbFirstBadged_update (K True) \<circ> mdbRevocable_update (K True));
setCTE slot makeObject
od)
 2. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q7 (emptySlot slot capability.NullCap) (do updateMDB (mdbPrev mdbn) (mdbNext_update (K 0) \<circ> mdbFirstBadged_update (K True) \<circ> mdbRevocable_update (K True));
setCTE slot makeObject
od)
 2. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and ?Q7) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q7 (do y <- clearUntypedFreeIndex slot;
newCTE <- getCTE slot;
case cteCap newCTE of capability.NullCap \<Rightarrow> return () | _ \<Rightarrow> do updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
updateCap slot capability.NullCap;
updateMDB slot (const nullMDBNode);
global.postCapDeletion capability.NullCap
od
od) (do y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>y. 0) \<circ> mdbFirstBadged_update (\<lambda>y. True) \<circ> mdbRevocable_update (\<lambda>y. True));
y <- updateCap slot (cteCap makeObject);
updateMDB slot (const (cteMDBNode makeObject))
od)
 2. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and ?Q7) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q11 (do newCTE <- getCTE slot;
case cteCap newCTE of capability.NullCap \<Rightarrow> return () | _ \<Rightarrow> do updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
updateCap slot capability.NullCap;
updateMDB slot (const nullMDBNode);
global.postCapDeletion capability.NullCap
od
od) (do y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>y. 0) \<circ> mdbFirstBadged_update (\<lambda>y. True) \<circ> mdbRevocable_update (\<lambda>y. True));
y <- updateCap slot (cteCap makeObject);
updateMDB slot (const (cteMDBNode makeObject))
od)
 2. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and ?Q11)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q22 (case cteCap cte of capability.NullCap \<Rightarrow> return () | _ \<Rightarrow> do updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode cte)));
updateMDB (mdbNext (cteMDBNode cte)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode cte)) mdb));
updateCap slot capability.NullCap;
updateMDB slot (const nullMDBNode);
global.postCapDeletion capability.NullCap
od) (do y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>y. 0) \<circ> mdbFirstBadged_update (\<lambda>y. True) \<circ> mdbRevocable_update (\<lambda>y. True));
y <- updateCap slot (cteCap makeObject);
updateMDB slot (const (cteMDBNode makeObject))
od)
 2. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 3. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q22 (do ctea <- getCTE (mdbPrev (cteMDBNode cte));
y <- setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. 0) (cteMDBNode ctea)) ctea);
y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
y <- setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte);
global.postCapDeletion capability.NullCap
od) (do ctea <- getCTE (mdbPrev (cteMDBNode cte));
y <- setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea);
y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od)
 2. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 3. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (4 subgoals):
 1. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q44 ctea) (do y <- setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. 0) (cteMDBNode ctea)) ctea);
y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
y <- setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte);
global.postCapDeletion capability.NullCap
od) (do y <- setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea);
y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od)
 2. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q22\<rbrace> getCTE (mdbPrev (cteMDBNode cte)) \<lbrace>?Q44\<rbrace>
 3. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 4. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (6 subgoals):
 1. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?P47 ctea) (setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. 0) (cteMDBNode ctea)) ctea)) (setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea))
 2. \<And>ctea y. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q47 ctea y) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
y <- setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte);
global.postCapDeletion capability.NullCap
od) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od)
 3. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R47 ctea\<rbrace> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea) \<lbrace>?Q47 ctea\<rbrace>
 4. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q22\<rbrace> getCTE (mdbPrev (cteMDBNode cte)) \<lbrace>\<lambda>cte. ?P47 cte and ?R47 cte\<rbrace>
 5. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 6. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (6 subgoals):
 1. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbFirstBadged (cteMDBNode ctea) \<and> mdbRevocable (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q51 ctea) (setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. 0) (cteMDBNode ctea)) ctea)) (setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea))
 2. \<And>ctea y. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q47 ctea y) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
y <- setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte);
global.postCapDeletion capability.NullCap
od) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od)
 3. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R47 ctea\<rbrace> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea) \<lbrace>?Q47 ctea\<rbrace>
 4. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q22\<rbrace> getCTE (mdbPrev (cteMDBNode cte)) \<lbrace>\<lambda>cte. (\<lambda>_. mdbFirstBadged (cteMDBNode cte) \<and> mdbRevocable (cteMDBNode cte)) and ?Q51 cte and ?R47 cte\<rbrace>
 5. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 6. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (6 subgoals):
 1. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbFirstBadged (cteMDBNode ctea) \<and> mdbRevocable (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. 0) (cteMDBNode ctea)) ctea) = setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea)
 2. \<And>ctea y. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q47 ctea y) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
y <- setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte);
global.postCapDeletion capability.NullCap
od) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od)
 3. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R47 ctea\<rbrace> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea) \<lbrace>?Q47 ctea\<rbrace>
 4. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q22\<rbrace> getCTE (mdbPrev (cteMDBNode cte)) \<lbrace>\<lambda>cte. (\<lambda>_. mdbFirstBadged (cteMDBNode cte) \<and> mdbRevocable (cteMDBNode cte)) and (\<lambda>_. True) and ?R47 cte\<rbrace>
 5. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 6. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (6 subgoals):
 1. \<And>ctea x1 mdbnode x1a x2 x3 x4. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbFirstBadged (cteMDBNode ctea) \<and> mdbRevocable (cteMDBNode ctea); ctea = CTE x1 mdbnode; mdbnode = MDB x1a x2 x3 x4\<rbrakk> \<Longrightarrow> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. 0) (cteMDBNode ctea)) ctea) = setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea)
 2. \<And>ctea y. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q47 ctea y) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
y <- setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte);
global.postCapDeletion capability.NullCap
od) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od)
 3. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R47 ctea\<rbrace> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea) \<lbrace>?Q47 ctea\<rbrace>
 4. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q22\<rbrace> getCTE (mdbPrev (cteMDBNode cte)) \<lbrace>\<lambda>cte. (\<lambda>_. mdbFirstBadged (cteMDBNode cte) \<and> mdbRevocable (cteMDBNode cte)) and (\<lambda>_. True) and ?R47 cte\<rbrace>
 5. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 6. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (5 subgoals):
 1. \<And>ctea y. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q47 ctea y) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
y <- setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte);
global.postCapDeletion capability.NullCap
od) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od)
 2. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R47 ctea\<rbrace> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea) \<lbrace>?Q47 ctea\<rbrace>
 3. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q22\<rbrace> getCTE (mdbPrev (cteMDBNode cte)) \<lbrace>\<lambda>cte. (\<lambda>_. mdbFirstBadged (cteMDBNode cte) \<and> mdbRevocable (cteMDBNode cte)) and (\<lambda>_. True) and ?R47 cte\<rbrace>
 4. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 5. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (5 subgoals):
 1. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q47 ctea ()) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od) (do y <- updateCap slot capability.NullCap;
cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. nullMDBNode) cte)
od)
 2. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R47 ctea\<rbrace> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea) \<lbrace>?Q47 ctea\<rbrace>
 3. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q22\<rbrace> getCTE (mdbPrev (cteMDBNode cte)) \<lbrace>\<lambda>cte. (\<lambda>_. mdbFirstBadged (cteMDBNode cte) \<and> mdbRevocable (cteMDBNode cte)) and (\<lambda>_. True) and ?R47 cte\<rbrace>
 4. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 5. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (4 subgoals):
 1. \<And>ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?R47 ctea\<rbrace> setCTE (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>y. 0) (mdbFirstBadged_update (\<lambda>y. True) (mdbRevocable_update (\<lambda>y. True) (cteMDBNode ctea)))) ctea) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q22\<rbrace> getCTE (mdbPrev (cteMDBNode cte)) \<lbrace>\<lambda>cte. (\<lambda>_. mdbFirstBadged (cteMDBNode cte) \<and> mdbRevocable (cteMDBNode cte)) and (\<lambda>_. True) and ?R47 cte\<rbrace>
 3. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; slot \<noteq> 0; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P22\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 4. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and (?P22 and ?Q22))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdbn = cteMDBNode cte; mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0; cteCap cte \<noteq> capability.NullCap; (cte_wp_at' ((=) cte) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev mdbn) and (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) and (\<lambda>s. no_0 (ctes_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. slot \<noteq> 0) and (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot and ((\<lambda>s. \<forall>ctea. cte_wp_at' ((=) ctea) slot s \<longrightarrow> ctea = cte) and (\<lambda>s. \<forall>ctea. cte_wp_at' ((=) ctea) (mdbPrev (cteMDBNode cte)) s \<longrightarrow> ((\<lambda>_. mdbFirstBadged (cteMDBNode ctea) \<and> mdbRevocable (cteMDBNode ctea)) and (\<lambda>_. True) and (\<lambda>s. True)) s)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ctea. \<lbrakk>mdbn = cteMDBNode cte; cteCap cte \<noteq> capability.NullCap; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0; ctes_of s slot = Some cte; isReplyCap (cteCap cte); \<forall>cte\<in>ran (ctes_of s). isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); no_0 (ctes_of s); ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea; isReplyCap (cteCap ctea); capReplyMaster (cteCap ctea)\<rbrakk> \<Longrightarrow> slot \<noteq> 0 \<and> \<not> isUntypedCap (cteCap cte) \<and> mdbFirstBadged (cteMDBNode ctea) \<and> mdbRevocable (cteMDBNode ctea) proof (prove)
goal:
No subgoals!