theory CSpace1_R

lemma by_products:
  "reply_masters_rvk_fb m = reply_masters_rvk_fb m'
 \<and> no_0 m = no_0 m' \<and> mdb_chain_0 m = mdb_chain_0 m'
 \<and> valid_nullcaps m = valid_nullcaps m'" apply (intro conjI) apply (simp add:ran_dom reply_masters_rvk_fb_def mdb_inv_preserve_def dom misc sameRegion mdb_next) apply (rule iffI) apply clarsimp apply (drule_tac x = y in bspec) apply (rule iffD2[OF dom]) apply clarsimp apply (frule iffD2[OF dom,OF domI],rotate_tac) apply (clarsimp simp:misc)+ apply (drule_tac x = y in bspec) apply (rule iffD1[OF dom]) apply clarsimp apply (frule iffD1[OF dom,OF domI],rotate_tac) apply (clarsimp simp:misc)+ apply (clarsimp simp:no_0_def) apply (rule ccontr) apply (simp add:dom_in) apply (subst (asm) dom[symmetric]) apply fastforce apply (rule iffI) apply (clarsimp simp:mdb_chain_0_def) apply (drule_tac x =x in bspec) apply (rule iffD2[OF dom],clarsimp) apply (erule_tac iffD1[OF connect_eqv_singleE,rotated]) apply (cut_tac p = p in mdb_next) apply (clarsimp simp: mdb_next_rel_def) apply (clarsimp simp:mdb_chain_0_def) apply (drule_tac x =x in bspec) apply (rule iffD1[OF dom],clarsimp) apply (erule_tac iffD1[OF connect_eqv_singleE,rotated]) apply (cut_tac p = p in mdb_next) apply (clarsimp simp: mdb_next_rel_def) apply (simp add:valid_nullcaps_def) apply (rule forall_eq,clarsimp)+ apply (rule iffI) apply clarsimp apply (frule iffD2[OF dom,OF domI]) apply (clarsimp) apply (case_tac y) apply (drule misc) apply assumption apply (clarsimp simp:isCap_simps) apply clarsimp apply (frule iffD1[OF dom,OF domI]) apply (clarsimp) apply (case_tac y) apply (drule misc) apply assumption apply (clarsimp simp:isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb m = reply_masters_rvk_fb m' \<and> no_0 m = no_0 m' \<and> mdb_chain_0 m = mdb_chain_0 m' \<and> valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (4 subgoals):
 1. reply_masters_rvk_fb m = reply_masters_rvk_fb m'
 2. no_0 m = no_0 m'
 3. mdb_chain_0 m = mdb_chain_0 m'
 4. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (4 subgoals):
 1. (\<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))) = (\<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))))
 2. no_0 m = no_0 m'
 3. mdb_chain_0 m = mdb_chain_0 m'
 4. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (5 subgoals):
 1. \<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y))) \<Longrightarrow> \<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y)))
 2. \<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))) \<Longrightarrow> \<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))
 3. no_0 m = no_0 m'
 4. mdb_chain_0 m = mdb_chain_0 m'
 5. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>\<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y))); m' y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya)\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 2. \<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))) \<Longrightarrow> \<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))
 3. no_0 m = no_0 m'
 4. mdb_chain_0 m = mdb_chain_0 m'
 5. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (6 subgoals):
 1. \<And>y ya. \<lbrakk>m' y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya)\<rbrakk> \<Longrightarrow> y \<in> dom m
 2. \<And>y ya. \<lbrakk>m' y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya); isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 3. \<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))) \<Longrightarrow> \<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))
 4. no_0 m = no_0 m'
 5. mdb_chain_0 m = mdb_chain_0 m'
 6. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (6 subgoals):
 1. \<And>y ya. \<lbrakk>m' y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya)\<rbrakk> \<Longrightarrow> y \<in> dom m'
 2. \<And>y ya. \<lbrakk>m' y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya); isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 3. \<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))) \<Longrightarrow> \<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))
 4. no_0 m = no_0 m'
 5. mdb_chain_0 m = mdb_chain_0 m'
 6. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>m' y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya); isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 2. \<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))) \<Longrightarrow> \<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))
 3. no_0 m = no_0 m'
 4. mdb_chain_0 m = mdb_chain_0 m'
 5. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>isReplyCap (cteCap ya); capReplyMaster (cteCap ya); isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y))); y \<in> dom m; m' y = Some ya\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 2. \<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))) \<Longrightarrow> \<forall>y\<in>dom m. isReplyCap (cteCap (the (m y))) \<and> capReplyMaster (cteCap (the (m y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m y))) \<and> mdbFirstBadged (cteMDBNode (the (m y)))
 3. no_0 m = no_0 m'
 4. mdb_chain_0 m = mdb_chain_0 m'
 5. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrakk>\<forall>y\<in>dom m'. isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))); m y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya)\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 2. no_0 m = no_0 m'
 3. mdb_chain_0 m = mdb_chain_0 m'
 4. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>m y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya)\<rbrakk> \<Longrightarrow> y \<in> dom m'
 2. \<And>y ya. \<lbrakk>m y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya); isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y)))\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 3. no_0 m = no_0 m'
 4. mdb_chain_0 m = mdb_chain_0 m'
 5. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>m y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya)\<rbrakk> \<Longrightarrow> y \<in> dom m
 2. \<And>y ya. \<lbrakk>m y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya); isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y)))\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 3. no_0 m = no_0 m'
 4. mdb_chain_0 m = mdb_chain_0 m'
 5. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrakk>m y = Some ya; isReplyCap (cteCap ya); capReplyMaster (cteCap ya); isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y)))\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 2. no_0 m = no_0 m'
 3. mdb_chain_0 m = mdb_chain_0 m'
 4. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrakk>isReplyCap (cteCap ya); capReplyMaster (cteCap ya); isReplyCap (cteCap (the (m' y))) \<and> capReplyMaster (cteCap (the (m' y))) \<longrightarrow> mdbRevocable (cteMDBNode (the (m' y))) \<and> mdbFirstBadged (cteMDBNode (the (m' y))); y \<in> dom m'; m y = Some ya\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode ya) \<and> mdbFirstBadged (cteMDBNode ya)
 2. no_0 m = no_0 m'
 3. mdb_chain_0 m = mdb_chain_0 m'
 4. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. no_0 m = no_0 m'
 2. mdb_chain_0 m = mdb_chain_0 m'
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. (m 0 = None) = (m' 0 = None)
 2. mdb_chain_0 m = mdb_chain_0 m'
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. (m 0 = None) \<noteq> (m' 0 = None) \<Longrightarrow> False
 2. mdb_chain_0 m = mdb_chain_0 m'
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. (m 0 = None) = (0 \<in> dom m') \<Longrightarrow> False
 2. mdb_chain_0 m = mdb_chain_0 m'
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. (m 0 = None) = (0 \<in> dom m) \<Longrightarrow> False
 2. mdb_chain_0 m = mdb_chain_0 m'
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (2 subgoals):
 1. mdb_chain_0 m = mdb_chain_0 m'
 2. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. mdb_chain_0 m \<Longrightarrow> mdb_chain_0 m'
 2. mdb_chain_0 m' \<Longrightarrow> mdb_chain_0 m
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; m' x = Some y\<rbrakk> \<Longrightarrow> m' \<turnstile> x \<leadsto>\<^sup>+ 0
 2. mdb_chain_0 m' \<Longrightarrow> mdb_chain_0 m
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (4 subgoals):
 1. \<And>x y. m' x = Some y \<Longrightarrow> x \<in> dom m
 2. \<And>x y. \<lbrakk>m' x = Some y; m \<turnstile> x \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m' \<turnstile> x \<leadsto>\<^sup>+ 0
 3. mdb_chain_0 m' \<Longrightarrow> mdb_chain_0 m
 4. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>m' x = Some y; m \<turnstile> x \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m' \<turnstile> x \<leadsto>\<^sup>+ 0
 2. mdb_chain_0 m' \<Longrightarrow> mdb_chain_0 m
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. \<And>x y p p'. m' x = Some y \<Longrightarrow> m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'
 2. mdb_chain_0 m' \<Longrightarrow> mdb_chain_0 m
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. \<And>x y p p'. \<lbrakk>m' x = Some y; mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'
 2. mdb_chain_0 m' \<Longrightarrow> mdb_chain_0 m
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (2 subgoals):
 1. mdb_chain_0 m' \<Longrightarrow> mdb_chain_0 m
 2. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom m'. m' \<turnstile> x \<leadsto>\<^sup>+ 0; m x = Some y\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ 0
 2. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (3 subgoals):
 1. \<And>x y. m x = Some y \<Longrightarrow> x \<in> dom m'
 2. \<And>x y. \<lbrakk>m x = Some y; m' \<turnstile> x \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ 0
 3. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>m x = Some y; m' \<turnstile> x \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ 0
 2. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (2 subgoals):
 1. \<And>x y p p'. m x = Some y \<Longrightarrow> m' \<turnstile> p \<leadsto> p' = m \<turnstile> p \<leadsto> p'
 2. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (2 subgoals):
 1. \<And>x y p p'. \<lbrakk>m x = Some y; mdb_next m p = mdb_next m' p\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' = m \<turnstile> p \<leadsto> p'
 2. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (1 subgoal):
 1. valid_nullcaps m = valid_nullcaps m' proof (prove)
goal (1 subgoal):
 1. (\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode) = (\<forall>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode) proof (prove)
goal (1 subgoal):
 1. \<And>p n. (m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode) = (m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode) proof (prove)
goal (2 subgoals):
 1. \<And>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode
 2. \<And>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode proof (prove)
goal (2 subgoals):
 1. \<And>p n. \<lbrakk>m' p = Some (CTE capability.NullCap n); m p \<noteq> Some (CTE capability.NullCap n)\<rbrakk> \<Longrightarrow> n = nullMDBNode
 2. \<And>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode proof (prove)
goal (2 subgoals):
 1. \<And>p n. \<lbrakk>m' p = Some (CTE capability.NullCap n); m p \<noteq> Some (CTE capability.NullCap n); p \<in> dom m\<rbrakk> \<Longrightarrow> n = nullMDBNode
 2. \<And>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode proof (prove)
goal (2 subgoals):
 1. \<And>p n y. \<lbrakk>m' p = Some (CTE capability.NullCap n); y \<noteq> CTE capability.NullCap n; m p = Some y\<rbrakk> \<Longrightarrow> n = nullMDBNode
 2. \<And>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode proof (prove)
goal (2 subgoals):
 1. \<And>p n y x1 x2. \<lbrakk>m' p = Some (CTE capability.NullCap n); y \<noteq> CTE capability.NullCap n; m p = Some y; y = CTE x1 x2\<rbrakk> \<Longrightarrow> n = nullMDBNode
 2. \<And>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode proof (prove)
goal (3 subgoals):
 1. \<And>p n y x1 x2. \<lbrakk>m' p = Some (CTE capability.NullCap n); y \<noteq> CTE capability.NullCap n; y = CTE x1 x2\<rbrakk> \<Longrightarrow> m' p = Some (?cte'154 p n y x1 x2)
 2. \<And>p n y x1 x2. \<lbrakk>m' p = Some (CTE capability.NullCap n); y \<noteq> CTE capability.NullCap n; y = CTE x1 x2; isUntypedCap (cteCap y) = isUntypedCap (cteCap (?cte'154 p n y x1 x2)) \<and> isNullCap (cteCap y) = isNullCap (cteCap (?cte'154 p n y x1 x2)) \<and> isReplyCap (cteCap y) = isReplyCap (cteCap (?cte'154 p n y x1 x2)) \<and> (isReplyCap (cteCap y) \<longrightarrow> capReplyMaster (cteCap y) = capReplyMaster (cteCap (?cte'154 p n y x1 x2))) \<and> isNotificationCap (cteCap y) = isNotificationCap (cteCap (?cte'154 p n y x1 x2)) \<and> (isNotificationCap (cteCap y) \<longrightarrow> capNtfnBadge (cteCap y) = capNtfnBadge (cteCap (?cte'154 p n y x1 x2))) \<and> isEndpointCap (cteCap y) = isEndpointCap (cteCap (?cte'154 p n y x1 x2)) \<and> (isEndpointCap (cteCap y) \<longrightarrow> capEPBadge (cteCap y) = capEPBadge (cteCap (?cte'154 p n y x1 x2))) \<and> untypedRange (cteCap y) = untypedRange (cteCap (?cte'154 p n y x1 x2)) \<and> capClass (cteCap y) = capClass (cteCap (?cte'154 p n y x1 x2)) \<and> isZombie (cteCap y) = isZombie (cteCap (?cte'154 p n y x1 x2)) \<and> isArchPageCap (cteCap y) = isArchPageCap (cteCap (?cte'154 p n y x1 x2)) \<and> capBits (cteCap y) = capBits (cteCap (?cte'154 p n y x1 x2)) \<and> global.capUntypedPtr (cteCap y) = global.capUntypedPtr (cteCap (?cte'154 p n y x1 x2)) \<and> capRange (cteCap y) = capRange (cteCap (?cte'154 p n y x1 x2)) \<and> isIRQControlCap (cteCap y) = isIRQControlCap (cteCap (?cte'154 p n y x1 x2)) \<and> cteMDBNode y = cteMDBNode (?cte'154 p n y x1 x2)\<rbrakk> \<Longrightarrow> n = nullMDBNode
 3. \<And>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode proof (prove)
goal (2 subgoals):
 1. \<And>p n y x1 x2. \<lbrakk>m' p = Some (CTE capability.NullCap n); y \<noteq> CTE capability.NullCap n; y = CTE x1 x2; isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE capability.NullCap n)) \<and> isNullCap (cteCap y) = isNullCap (cteCap (CTE capability.NullCap n)) \<and> isReplyCap (cteCap y) = isReplyCap (cteCap (CTE capability.NullCap n)) \<and> (isReplyCap (cteCap y) \<longrightarrow> capReplyMaster (cteCap y) = capReplyMaster (cteCap (CTE capability.NullCap n))) \<and> isNotificationCap (cteCap y) = isNotificationCap (cteCap (CTE capability.NullCap n)) \<and> (isNotificationCap (cteCap y) \<longrightarrow> capNtfnBadge (cteCap y) = capNtfnBadge (cteCap (CTE capability.NullCap n))) \<and> isEndpointCap (cteCap y) = isEndpointCap (cteCap (CTE capability.NullCap n)) \<and> (isEndpointCap (cteCap y) \<longrightarrow> capEPBadge (cteCap y) = capEPBadge (cteCap (CTE capability.NullCap n))) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE capability.NullCap n)) \<and> capClass (cteCap y) = capClass (cteCap (CTE capability.NullCap n)) \<and> isZombie (cteCap y) = isZombie (cteCap (CTE capability.NullCap n)) \<and> isArchPageCap (cteCap y) = isArchPageCap (cteCap (CTE capability.NullCap n)) \<and> capBits (cteCap y) = capBits (cteCap (CTE capability.NullCap n)) \<and> global.capUntypedPtr (cteCap y) = global.capUntypedPtr (cteCap (CTE capability.NullCap n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE capability.NullCap n)) \<and> isIRQControlCap (cteCap y) = isIRQControlCap (cteCap (CTE capability.NullCap n)) \<and> cteMDBNode y = cteMDBNode (CTE capability.NullCap n)\<rbrakk> \<Longrightarrow> n = nullMDBNode
 2. \<And>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. m' p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode \<Longrightarrow> m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>m p = Some (CTE capability.NullCap n); m' p \<noteq> Some (CTE capability.NullCap n)\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>m p = Some (CTE capability.NullCap n); m' p \<noteq> Some (CTE capability.NullCap n); p \<in> dom m'\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n y. \<lbrakk>m p = Some (CTE capability.NullCap n); y \<noteq> CTE capability.NullCap n; m' p = Some y\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n y x1 x2. \<lbrakk>m p = Some (CTE capability.NullCap n); y \<noteq> CTE capability.NullCap n; m' p = Some y; y = CTE x1 x2\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (2 subgoals):
 1. \<And>p n y x1 x2. \<lbrakk>y \<noteq> CTE capability.NullCap n; m' p = Some y; y = CTE x1 x2\<rbrakk> \<Longrightarrow> m' p = Some (?cte'165 p n y x1 x2)
 2. \<And>p n y x1 x2. \<lbrakk>y \<noteq> CTE capability.NullCap n; m' p = Some y; y = CTE x1 x2; isUntypedCap (cteCap (CTE capability.NullCap n)) = isUntypedCap (cteCap (?cte'165 p n y x1 x2)) \<and> isNullCap (cteCap (CTE capability.NullCap n)) = isNullCap (cteCap (?cte'165 p n y x1 x2)) \<and> isReplyCap (cteCap (CTE capability.NullCap n)) = isReplyCap (cteCap (?cte'165 p n y x1 x2)) \<and> (isReplyCap (cteCap (CTE capability.NullCap n)) \<longrightarrow> capReplyMaster (cteCap (CTE capability.NullCap n)) = capReplyMaster (cteCap (?cte'165 p n y x1 x2))) \<and> isNotificationCap (cteCap (CTE capability.NullCap n)) = isNotificationCap (cteCap (?cte'165 p n y x1 x2)) \<and> (isNotificationCap (cteCap (CTE capability.NullCap n)) \<longrightarrow> capNtfnBadge (cteCap (CTE capability.NullCap n)) = capNtfnBadge (cteCap (?cte'165 p n y x1 x2))) \<and> isEndpointCap (cteCap (CTE capability.NullCap n)) = isEndpointCap (cteCap (?cte'165 p n y x1 x2)) \<and> (isEndpointCap (cteCap (CTE capability.NullCap n)) \<longrightarrow> capEPBadge (cteCap (CTE capability.NullCap n)) = capEPBadge (cteCap (?cte'165 p n y x1 x2))) \<and> untypedRange (cteCap (CTE capability.NullCap n)) = untypedRange (cteCap (?cte'165 p n y x1 x2)) \<and> capClass (cteCap (CTE capability.NullCap n)) = capClass (cteCap (?cte'165 p n y x1 x2)) \<and> isZombie (cteCap (CTE capability.NullCap n)) = isZombie (cteCap (?cte'165 p n y x1 x2)) \<and> isArchPageCap (cteCap (CTE capability.NullCap n)) = isArchPageCap (cteCap (?cte'165 p n y x1 x2)) \<and> capBits (cteCap (CTE capability.NullCap n)) = capBits (cteCap (?cte'165 p n y x1 x2)) \<and> global.capUntypedPtr (cteCap (CTE capability.NullCap n)) = global.capUntypedPtr (cteCap (?cte'165 p n y x1 x2)) \<and> capRange (cteCap (CTE capability.NullCap n)) = capRange (cteCap (?cte'165 p n y x1 x2)) \<and> isIRQControlCap (cteCap (CTE capability.NullCap n)) = isIRQControlCap (cteCap (?cte'165 p n y x1 x2)) \<and> cteMDBNode (CTE capability.NullCap n) = cteMDBNode (?cte'165 p n y x1 x2)\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n y x1 x2. \<lbrakk>y \<noteq> CTE capability.NullCap n; m' p = Some y; y = CTE x1 x2; isUntypedCap (cteCap (CTE capability.NullCap n)) = isUntypedCap (cteCap y) \<and> isNullCap (cteCap (CTE capability.NullCap n)) = isNullCap (cteCap y) \<and> isReplyCap (cteCap (CTE capability.NullCap n)) = isReplyCap (cteCap y) \<and> (isReplyCap (cteCap (CTE capability.NullCap n)) \<longrightarrow> capReplyMaster (cteCap (CTE capability.NullCap n)) = capReplyMaster (cteCap y)) \<and> isNotificationCap (cteCap (CTE capability.NullCap n)) = isNotificationCap (cteCap y) \<and> (isNotificationCap (cteCap (CTE capability.NullCap n)) \<longrightarrow> capNtfnBadge (cteCap (CTE capability.NullCap n)) = capNtfnBadge (cteCap y)) \<and> isEndpointCap (cteCap (CTE capability.NullCap n)) = isEndpointCap (cteCap y) \<and> (isEndpointCap (cteCap (CTE capability.NullCap n)) \<longrightarrow> capEPBadge (cteCap (CTE capability.NullCap n)) = capEPBadge (cteCap y)) \<and> untypedRange (cteCap (CTE capability.NullCap n)) = untypedRange (cteCap y) \<and> capClass (cteCap (CTE capability.NullCap n)) = capClass (cteCap y) \<and> isZombie (cteCap (CTE capability.NullCap n)) = isZombie (cteCap y) \<and> isArchPageCap (cteCap (CTE capability.NullCap n)) = isArchPageCap (cteCap y) \<and> capBits (cteCap (CTE capability.NullCap n)) = capBits (cteCap y) \<and> global.capUntypedPtr (cteCap (CTE capability.NullCap n)) = global.capUntypedPtr (cteCap y) \<and> capRange (cteCap (CTE capability.NullCap n)) = capRange (cteCap y) \<and> isIRQControlCap (cteCap (CTE capability.NullCap n)) = isIRQControlCap (cteCap y) \<and> cteMDBNode (CTE capability.NullCap n) = cteMDBNode y\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal:
No subgoals!