theory Finalise_R

lemma isFinal:
  "\<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) cte) x s
          \<and> final_matters' (cteCap cte)
          \<and> Q (isFinal (cteCap cte) x (cteCaps_of s)) s\<rbrace>
    isFinalCapability cte
   \<lbrace>Q\<rbrace>" unfolding isFinalCapability_def apply (cases cte) apply (rename_tac cap node) apply (unfold Let_def) apply (simp only: if_False) apply (wp getCTE_wp') apply (cases "mdbPrev (cteMDBNode cte) = nullPointer") apply simp apply (clarsimp simp: valid_mdb_ctes_def valid_mdb'_def
                         cte_wp_at_ctes_of) apply (rule conjI, clarsimp simp: nullPointer_def) apply (erule rsubst[where P="\<lambda>x. Q x s" for s], simp) apply (rule classical) apply (drule(5) notFinal_prev_or_next) apply clarsimp apply (clarsimp simp: nullPointer_def) apply (erule rsubst[where P="\<lambda>x. Q x s" for s]) apply (rule sym, rule iffI) apply (rule classical) apply (drule(5) notFinal_prev_or_next) apply clarsimp apply clarsimp apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) apply (case_tac cte) apply clarsimp apply (clarsimp simp add: isFinal_def) apply (erule_tac x="mdbNext node" in allE) apply simp apply (erule impE) apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def) apply (drule (1) mdb_chain_0_no_loops) apply simp apply (clarsimp simp: sameObjectAs_def3 isCap_simps) apply simp apply (clarsimp simp: cte_wp_at_ctes_of
                        valid_mdb_ctes_def valid_mdb'_def) apply (case_tac cte) apply clarsimp apply (rule conjI) apply clarsimp apply (erule rsubst[where P="\<lambda>x. Q x s" for s]) apply clarsimp apply (clarsimp simp: isFinal_def cteCaps_of_def) apply (erule_tac x="mdbPrev node" in allE) apply simp apply (erule impE) apply clarsimp apply (drule (1) mdb_chain_0_no_loops) apply (subgoal_tac "ctes_of s (mdbNext node) = Some (CTE cap node)") apply clarsimp apply (erule (1) valid_dlistEp) apply clarsimp apply (case_tac cte') apply clarsimp apply (clarsimp simp add: sameObjectAs_def3 isCap_simps) apply clarsimp apply (rule conjI) apply clarsimp apply (erule rsubst[where P="\<lambda>x. Q x s" for s], simp) apply (rule classical, drule(5) notFinal_prev_or_next) apply (clarsimp simp: sameObjectAs_sym nullPointer_def) apply (clarsimp simp: nullPointer_def) apply (erule rsubst[where P="\<lambda>x. Q x s" for s]) apply (rule sym, rule iffI) apply (rule classical, drule(5) notFinal_prev_or_next) apply (clarsimp simp: sameObjectAs_sym) apply auto[1] apply (clarsimp simp: isFinal_def cteCaps_of_def) apply (case_tac cte) apply (erule_tac x="mdbNext node" in allE) apply simp apply (erule impE) apply clarsimp apply (drule (1) mdb_chain_0_no_loops) apply simp apply clarsimp apply (clarsimp simp: isCap_simps sameObjectAs_def3) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) cte) x s \<and> final_matters' (cteCap cte) \<and> Q (isFinal (cteCap cte) x (cteCaps_of s)) s\<rbrace> isFinalCapability cte \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) cte) x s \<and> final_matters' (cteCap cte) \<and> Q (isFinal (cteCap cte) x (cteCaps_of s)) s\<rbrace> let cte = cte; mdb = cteMDBNode cte in do prevIsSameObject <- if mdbPrev mdb = nullPointer then return False else do prev <- getCTE (mdbPrev mdb);
return $ global.sameObjectAs (cteCap prev) (cteCap cte)
od;
if prevIsSameObject then return False else if mdbNext mdb = nullPointer then return True else do next <- getCTE (mdbNext mdb);
return $ Not $ global.sameObjectAs (cteCap cte) (cteCap next)
od
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. cte = CTE x1 x2 \<Longrightarrow> \<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) cte) x s \<and> final_matters' (cteCap cte) \<and> Q (isFinal (cteCap cte) x (cteCaps_of s)) s\<rbrace> let cte = cte; mdb = cteMDBNode cte in do prevIsSameObject <- if mdbPrev mdb = nullPointer then return False else do prev <- getCTE (mdbPrev mdb);
return $ global.sameObjectAs (cteCap prev) (cteCap cte)
od;
if prevIsSameObject then return False else if mdbNext mdb = nullPointer then return True else do next <- getCTE (mdbNext mdb);
return $ Not $ global.sameObjectAs (cteCap cte) (cteCap next)
od
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap node. cte = CTE cap node \<Longrightarrow> \<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) cte) x s \<and> final_matters' (cteCap cte) \<and> Q (isFinal (cteCap cte) x (cteCaps_of s)) s\<rbrace> let cte = cte; mdb = cteMDBNode cte in do prevIsSameObject <- if mdbPrev mdb = nullPointer then return False else do prev <- getCTE (mdbPrev mdb);
return $ global.sameObjectAs (cteCap prev) (cteCap cte)
od;
if prevIsSameObject then return False else if mdbNext mdb = nullPointer then return True else do next <- getCTE (mdbNext mdb);
return $ Not $ global.sameObjectAs (cteCap cte) (cteCap next)
od
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap node. cte = CTE cap node \<Longrightarrow> \<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) cte) x s \<and> final_matters' (cteCap cte) \<and> Q (isFinal (cteCap cte) x (cteCaps_of s)) s\<rbrace> do prevIsSameObject <- if mdbPrev (cteMDBNode cte) = nullPointer then return False else do prev <- getCTE (mdbPrev (cteMDBNode cte));
return $ global.sameObjectAs (cteCap prev) (cteCap cte)
od;
if prevIsSameObject then return False else if mdbNext (cteMDBNode cte) = nullPointer then return True else do next <- getCTE (mdbNext (cteMDBNode cte));
return $ Not $ global.sameObjectAs (cteCap cte) (cteCap next)
od
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap node. cte = CTE cap node \<Longrightarrow> \<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s\<rbrace> do prevIsSameObject <- if mdbPrev (cteMDBNode (CTE cap node)) = nullPointer then return False else do prev <- getCTE (mdbPrev (cteMDBNode (CTE cap node)));
return $ global.sameObjectAs (cteCap prev) (cteCap (CTE cap node))
od;
if prevIsSameObject then return False else if mdbNext (cteMDBNode (CTE cap node)) = nullPointer then return True else do next <- getCTE (mdbNext (cteMDBNode (CTE cap node)));
return $ Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap next)
od
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))))
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' cap \<and> Q (isFinal cap x (cteCaps_of s)) s; mdbPrev node = nullPointer\<rbrakk> \<Longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext node) s \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s))
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s\<rbrakk> \<Longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s))
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; mdbNext node = 0\<rbrakk> \<Longrightarrow> Q True s
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node = 0\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node = 0; \<not> isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node = 0; (\<exists>cap' node'. ctes_of s (mdbPrev node) = Some (CTE cap' node') \<and> global.sameObjectAs cap cap') \<or> (\<exists>cap' node'. ctes_of s (mdbNext node) = Some (CTE cap' node') \<and> global.sameObjectAs cap cap')\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; mdbPrev node = nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea\<rbrakk> \<Longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap ctea)) s
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s) = (\<not> global.sameObjectAs cap (cteCap ctea))
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; \<not> global.sameObjectAs cap (cteCap ctea); \<not> isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; \<not> global.sameObjectAs cap (cteCap ctea); (\<exists>cap' node'. ctes_of s (mdbPrev node) = Some (CTE cap' node') \<and> global.sameObjectAs cap cap') \<or> (\<exists>cap' node'. ctes_of s (mdbNext node) = Some (CTE cap' node') \<and> global.sameObjectAs cap cap')\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; isFinal cap x (cteCaps_of s); global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; isFinal cap x (map_option cteCap \<circ> ctes_of s); global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea x1 x2. \<lbrakk>cte = CTE cap node; mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; isFinal cap x (map_option cteCap \<circ> ctes_of s); global.sameObjectAs cap (cteCap ctea); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; isFinal cap x (map_option cteCap \<circ> ctes_of s); global.sameObjectAs cap (cteCap ctea); cte = CTE cap node\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; global.sameObjectAs cap (cteCap ctea); cte = CTE cap node; \<not> isUntypedCap cap; \<forall>p' c. (\<exists>z. ctes_of s p' = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; global.sameObjectAs cap (cteCap ctea); cte = CTE cap node; \<not> isUntypedCap cap; \<forall>c. (\<exists>z. ctes_of s (mdbNext node) = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> mdbNext node \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; global.sameObjectAs cap (cteCap ctea); cte = CTE cap node; \<not> isUntypedCap cap; x \<noteq> mdbNext node \<longrightarrow> isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; global.sameObjectAs cap (cteCap ctea); cte = CTE cap node; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> x \<noteq> mdbNext node
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; global.sameObjectAs cap (cteCap ctea); cte = CTE cap node; \<not> isUntypedCap cap; isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some (CTE cap node); global.sameObjectAs cap cap; cte = CTE cap node; \<not> isUntypedCap cap; x = mdbNext node\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; global.sameObjectAs cap (cteCap ctea); cte = CTE cap node; \<not> isUntypedCap cap; isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some (CTE cap node); global.sameObjectAs cap cap; cte = CTE cap node; \<not> isUntypedCap cap; x = mdbNext node; no_loops (ctes_of s)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; global.sameObjectAs cap (cteCap ctea); cte = CTE cap node; \<not> isUntypedCap cap; isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node = 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some ctea; global.sameObjectAs cap (cteCap ctea); cte = CTE cap node; \<not> isUntypedCap cap; isUntypedCap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' (cteCap (CTE cap node)) \<and> Q (isFinal (cteCap (CTE cap node)) x (cteCaps_of s)) s; mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> (False \<longrightarrow> Q False s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s)))) \<and> (mdbPrev (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbPrev (cteMDBNode (CTE cap node))) s \<longrightarrow> (global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) (cteCap (CTE cap node)) \<longrightarrow> (mdbNext (cteMDBNode (CTE cap node)) = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext (cteMDBNode (CTE cap node)) \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext (cteMDBNode (CTE cap node))) s \<longrightarrow> Q (Not $ global.sameObjectAs (cteCap (CTE cap node)) (cteCap cte)) s))))) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s. \<lbrakk>cte = CTE cap node; valid_mdb' s \<and> cte_wp_at' ((=) (CTE cap node)) x s \<and> final_matters' cap \<and> Q (isFinal cap x (cteCaps_of s)) s; mdbPrev node \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (mdbPrev node) s \<longrightarrow> (global.sameObjectAs (cteCap cte) cap \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap cte) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (mdbNext node) s \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s))) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea. \<lbrakk>cte = CTE cap node; mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea\<rbrakk> \<Longrightarrow> (global.sameObjectAs (cteCap ctea) cap \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s))) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea x1 x2. \<lbrakk>cte = CTE cap node; mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> (global.sameObjectAs (cteCap ctea) cap \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s))) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> (global.sameObjectAs (cteCap ctea) cap \<longrightarrow> Q False s) \<and> (\<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s))) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> Q False s
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> Q False s
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s) = False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<forall>p' c. (\<exists>z. ctes_of s p' = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<forall>c. (\<exists>z. ctes_of s (mdbPrev node) = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> mdbPrev node \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; x \<noteq> mdbPrev node \<longrightarrow> \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> x \<noteq> mdbPrev node
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node; no_loops (ctes_of s)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (4 subgoals):
 1. \<And>cap node s. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node; no_loops (ctes_of s); ctes_of s (mdbNext node) = Some (CTE cap node)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node; no_loops (ctes_of s)\<rbrakk> \<Longrightarrow> ctes_of s (mdbNext node) = Some (CTE cap node)
 3. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 4. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node; no_loops (ctes_of s)\<rbrakk> \<Longrightarrow> ctes_of s (mdbNext node) = Some (CTE cap node)
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (4 subgoals):
 1. \<And>cap node s. \<lbrakk>mdbPrev node \<noteq> nullPointer; no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node; no_loops (ctes_of s)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (CTE cap node)) \<noteq> 0
 2. \<And>cap node s cte'. \<lbrakk>mdbPrev node \<noteq> nullPointer; no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node; no_loops (ctes_of s); ctes_of s (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = mdbPrev node\<rbrakk> \<Longrightarrow> ctes_of s (mdbNext node) = Some (CTE cap node)
 3. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 4. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s cte'. \<lbrakk>mdbPrev node \<noteq> nullPointer; no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node; no_loops (ctes_of s); ctes_of s (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = mdbPrev node\<rbrakk> \<Longrightarrow> ctes_of s (mdbNext node) = Some (CTE cap node)
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (3 subgoals):
 1. \<And>cap node s cte' x1 x2. \<lbrakk>mdbPrev node \<noteq> nullPointer; no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some (CTE cap node); cte = CTE cap node; global.sameObjectAs cap cap; \<not> isUntypedCap cap; x = mdbPrev node; no_loops (ctes_of s); ctes_of s (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = mdbPrev node; cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> ctes_of s (mdbNext node) = Some (CTE cap node)
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; global.sameObjectAs (cteCap ctea) cap; \<not> isUntypedCap cap; \<not> isUntypedCap (cteCap ctea) \<longrightarrow> \<not> global.sameObjectAs cap (cteCap ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs (cteCap ctea) cap \<longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> (mdbNext node = nullPointer \<longrightarrow> Q True s) \<and> (mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> mdbNext node = nullPointer \<longrightarrow> Q True s
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node = nullPointer\<rbrakk> \<Longrightarrow> Q True s
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node = nullPointer\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node = nullPointer; (\<exists>cap' node'. ctes_of s (mdbPrev node) = Some (CTE cap' node') \<and> global.sameObjectAs cap cap') \<or> (\<exists>cap' node'. ctes_of s (mdbNext node) = Some (CTE cap' node') \<and> global.sameObjectAs cap cap')\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> nullPointer; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap\<rbrakk> \<Longrightarrow> mdbNext node \<noteq> nullPointer \<longrightarrow> (\<forall>cte. ctes_of s (mdbNext node) = Some cte \<longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cte)) s) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; Q (isFinal cap x (cteCaps_of s)) s; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa\<rbrakk> \<Longrightarrow> Q (\<not> global.sameObjectAs cap (cteCap cteaa)) s proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s) = (\<not> global.sameObjectAs cap (cteCap cteaa)) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> global.sameObjectAs cap (cteCap cteaa)\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap cteaa) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> global.sameObjectAs cap (cteCap cteaa); (\<exists>cap' node'. ctes_of s (mdbPrev node) = Some (CTE cap' node') \<and> global.sameObjectAs cap cap') \<or> (\<exists>cap' node'. ctes_of s (mdbNext node) = Some (CTE cap' node') \<and> global.sameObjectAs cap cap')\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap cteaa) proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs cap (cteCap ctea); mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> global.sameObjectAs cap (cteCap cteaa); (\<exists>cap'. (\<exists>node'. ctea = CTE cap' node') \<and> global.sameObjectAs cap cap') \<or> (\<exists>cap'. (\<exists>node'. cteaa = CTE cap' node') \<and> global.sameObjectAs cap cap')\<rbrakk> \<Longrightarrow> isFinal cap x (cteCaps_of s)
 2. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap cteaa) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; isFinal cap x (cteCaps_of s)\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap cteaa) proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; \<forall>p' c. (\<exists>z. ctes_of s p' = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c; global.sameObjectAs cap (cteCap cteaa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa x1 x2. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; \<forall>p' c. (\<exists>z. ctes_of s p' = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c; global.sameObjectAs cap (cteCap cteaa); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa x1 x2. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; cte = CTE cap node; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cteaa); cte = CTE x1 x2; \<forall>c. (\<exists>z. ctes_of s (mdbNext node) = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> mdbNext node \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa x1. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; x1 = cap; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cteaa); cte = CTE cap node; x \<noteq> mdbNext node \<longrightarrow> isUntypedCap (cteCap cteaa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea cteaa x1. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; x1 = cap; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cteaa); cte = CTE cap node\<rbrakk> \<Longrightarrow> x \<noteq> mdbNext node
 2. \<And>cap node s ctea cteaa x1. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; x1 = cap; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cteaa); cte = CTE cap node; isUntypedCap (cteCap cteaa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some (CTE cap node); \<not> isUntypedCap cap; global.sameObjectAs cap cap; cte = CTE cap node; x = mdbNext node\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea cteaa x1. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; x1 = cap; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cteaa); cte = CTE cap node; isUntypedCap (cteCap cteaa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap node s ctea. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some (CTE cap node); \<not> isUntypedCap cap; global.sameObjectAs cap cap; cte = CTE cap node; x = mdbNext node; no_loops (ctes_of s)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap node s ctea cteaa x1. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; x1 = cap; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cteaa); cte = CTE cap node; isUntypedCap (cteCap cteaa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa x1. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; x1 = cap; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cteaa); cte = CTE cap node; isUntypedCap (cteCap cteaa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap node s ctea cteaa. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE cap node); final_matters' cap; ctes_of s (mdbPrev node) = Some ctea; \<not> global.sameObjectAs (cteCap ctea) cap; mdbNext node \<noteq> 0; ctes_of s (mdbNext node) = Some cteaa; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cteaa); cte = CTE cap node; isUntypedCap (cteCap cteaa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!