theory Finalise_R

lemma valid_badges_n:
  "valid_badges n" proof - from valid_badges show ?thesis apply (simp add: valid_badges_def2) apply clarsimp apply (drule_tac p=p in n_cap) apply (frule n_cap) apply (drule n_badged) apply (clarsimp simp: n_next_eq) apply (case_tac "p=slot", simp) apply clarsimp apply (case_tac "p'=slot", simp) apply clarsimp apply (case_tac "p = mdbPrev s_node") apply clarsimp apply (insert slot)[1] 
     (* using mdb_chunked to show cap in between is same as on either side *)
      apply (subgoal_tac "capMasterCap s_cap = capMasterCap cap'") prefer 2 apply (thin_tac "\<forall>p. P p" for P) apply (drule mdb_chunked2D[OF chunked]) apply (fastforce simp: mdb_next_unfold) apply assumption+ apply (simp add: sameRegionAs_def3) apply (intro disjI1) apply (fastforce simp:isCap_simps capMasterCap_def split:capability.splits) apply clarsimp apply clarsimp apply (erule sameRegionAsE, auto simp: isCap_simps capMasterCap_def split:capability.splits)[1] 
     (* instantiating known valid_badges on both sides to transitively
        give the link we need *)
      apply (frule_tac x="mdbPrev s_node" in spec) apply simp apply (drule spec, drule spec, drule spec,
            drule(1) mp, drule(1) mp) apply simp apply (drule_tac x=slot in spec) apply (drule_tac x="mdbNext s_node" in spec) apply simp apply (drule mp, simp(no_asm) add: mdb_next_unfold) apply simp apply (cases "capBadge s_cap", simp_all)[1] apply clarsimp apply (case_tac "p' = mdbNext s_node") apply clarsimp apply (frule vdlist_next_src_unique[where y=slot]) apply (simp add: mdb_next_unfold slot) apply clarsimp apply (rule dlist) apply clarsimp apply clarsimp apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_badges n proof (state)
goal (1 subgoal):
 1. valid_badges n proof (chain)
picking this:
valid_badges m proof (prove)
using this:
valid_badges m

goal (1 subgoal):
 1. valid_badges n proof (prove)
goal (1 subgoal):
 1. \<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node') \<Longrightarrow> \<forall>p p' cap. (\<exists>node. n p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. n p' = Some (CTE cap' node') \<longrightarrow> n \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' y. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); n p = Some (CTE cap node); n p' = Some (CTE cap' node'); n \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' y. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); n p' = Some (CTE cap' node'); n \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then cap = capability.NullCap else cap' = cap)\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' y. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); n p' = Some (CTE cap' node'); n \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then cap = capability.NullCap else cap' = cap); \<exists>cap'a node'. m p' = Some (CTE cap'a node') \<and> (if p' = slot then cap' = capability.NullCap else cap'a = cap')\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' y. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); n \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then cap = capability.NullCap else cap' = cap); \<exists>cap'a node'. m p' = Some (CTE cap'a node') \<and> (if p' = slot then cap' = capability.NullCap else cap'a = cap'); \<exists>cap' node'a. m p' = Some (CTE cap' node'a) \<and> (if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a)\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' y cap'a cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = slot then p' = 0 else if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; if p = slot then cap = capability.NullCap else cap'a = cap; m p = Some (CTE cap'a node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' y cap'a cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = slot then p' = 0 else if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; if p = slot then cap = capability.NullCap else cap'a = cap; m p = Some (CTE cap'a node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then False else m \<turnstile> p \<leadsto> slot; capMasterCap cap = capability.NullCap; capBadge cap = Some y; m p = Some (CTE cap node'b); cap' = capability.NullCap; m slot = Some (CTE cap'b node'a); \<not> mdbFirstBadged node'; p \<noteq> slot; p' = slot\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node'
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (3 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 3. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (3 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (3 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (8 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> ?p''72 cap cap' node' y node'a node'b
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> m (mdbPrev s_node) = Some (CTE (?cap72 cap cap' node' y node'a node'b) (?nd72 cap cap' node' y node'a node'b))
 3. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> m (?p''72 cap cap' node' y node'a node'b) = Some (CTE (?cap''72 cap cap' node' y node'a node'b) (?nd''72 cap cap' node' y node'a node'b))
 4. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> global.sameRegionAs (?cap72 cap cap' node' y node'a node'b) (?cap''72 cap cap' node' y node'a node'b)
 5. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> ?p''72 cap cap' node' y node'a node'b
 6. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); \<exists>cap'a nd'. m slot = Some (CTE cap'a nd') \<and> global.sameRegionAs (?cap72 cap cap' node' y node'a node'b) cap'a\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 7. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 8. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (7 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> m (mdbPrev s_node) = Some (CTE (?cap72 cap cap' node' y node'a node'b) (?nd72 cap cap' node' y node'a node'b))
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> m (mdbNext s_node) = Some (CTE (?cap''72 cap cap' node' y node'a node'b) (?nd''72 cap cap' node' y node'a node'b))
 3. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> global.sameRegionAs (?cap72 cap cap' node' y node'a node'b) (?cap''72 cap cap' node' y node'a node'b)
 4. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node
 5. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); \<exists>cap'a nd'. m slot = Some (CTE cap'a nd') \<and> global.sameRegionAs (?cap72 cap cap' node' y node'a node'b) cap'a\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 6. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 7. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (5 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node
 3. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); \<exists>cap' nd'. m slot = Some (CTE cap' nd') \<and> global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 4. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 5. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (5 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap'
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node
 3. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); \<exists>cap' nd'. m slot = Some (CTE cap' nd') \<and> global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 4. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 5. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (5 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap'
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node
 3. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); \<exists>cap' nd'. m slot = Some (CTE cap' nd') \<and> global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 4. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 5. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (4 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); \<exists>cap' nd'. m slot = Some (CTE cap' nd') \<and> global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 3. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 4. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (3 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); \<exists>cap' nd'. m slot = Some (CTE cap' nd') \<and> global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (3 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); global.sameRegionAs cap s_cap\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap'
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; \<forall>p' cap. (\<exists>node. m (mdbPrev s_node) = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; \<forall>p' cap'a node'. m p' = Some (CTE cap'a node') \<longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> p' \<longrightarrow> capMasterCap cap' = capMasterCap cap'a \<longrightarrow> Some y \<noteq> capBadge cap'a \<longrightarrow> capBadge cap'a \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; capMasterCap cap' = capMasterCap s_cap \<longrightarrow> Some y \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap \<noteq> Some 0 \<longrightarrow> mdbFirstBadged s_node\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; Some y \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap = Some 0\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; Some y \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap = Some 0; \<forall>p' cap. (\<exists>node. m slot = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> slot \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; Some y \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap = Some 0; \<forall>cap. (\<exists>node. m slot = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; Some y \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap = Some 0; m \<turnstile> slot \<leadsto> mdbNext s_node \<longrightarrow> (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap = capBadge cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (3 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; Some y \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap = Some 0\<rbrakk> \<Longrightarrow> \<exists>z. m slot = Some z \<and> mdbNext s_node = mdbNext (cteMDBNode z)
 2. \<And>cap cap' node' y node'a node'b. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; Some y \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap = Some 0; (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap = capBadge cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>cap cap' node' y node'a node'b. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> slot; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m (mdbPrev s_node) = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; m slot = Some (CTE s_cap s_node); capMasterCap s_cap = capMasterCap cap'; Some y \<noteq> capBadge s_cap \<longrightarrow> capBadge s_cap = Some 0; (\<exists>y. capBadge s_cap = Some y) \<longrightarrow> capBadge s_cap = capBadge cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' y cap'b node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); if p = mdbPrev s_node then m \<turnstile> mdbPrev s_node \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); if p' = slot then cap' = capability.NullCap else cap'b = cap'; m p' = Some (CTE cap'b node'a); if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node'
 2. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (5 subgoals):
 1. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 2. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 3. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> valid_dlist m
 4. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; p = slot\<rbrakk> \<Longrightarrow> False
 5. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (4 subgoals):
 1. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 2. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; p = slot\<rbrakk> \<Longrightarrow> False
 4. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (3 subgoals):
 1. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; p = slot\<rbrakk> \<Longrightarrow> False
 3. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (2 subgoals):
 1. \<And>p cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> mdbNext s_node; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m (mdbNext s_node) = Some (CTE cap' node'a); p \<noteq> slot; p \<noteq> mdbPrev s_node; \<not> mdbFirstBadged s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a; p = slot\<rbrakk> \<Longrightarrow> False
 2. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged node'a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged node'a; p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' y node'a node'b. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node'); m \<turnstile> p \<leadsto> p'; capMasterCap cap = capMasterCap cap'; capBadge cap = Some y; Some y \<noteq> capBadge cap'; capBadge cap' \<noteq> Some 0; m p = Some (CTE cap node'b); m p' = Some (CTE cap' node'a); p \<noteq> slot; p' \<noteq> slot; p \<noteq> mdbPrev s_node; p' \<noteq> mdbNext s_node; \<not> mdbFirstBadged node'; \<not> mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
valid_badges n

goal:
No subgoals!