theory CSpace1_R

lemma (in mdb_insert_der) dest_no_parent_n:
  "n \<turnstile> dest \<rightarrow> p = False" using src partial_is_derived' valid_badges ut_rev apply clarsimp apply (erule subtree.induct) prefer 2 apply simp apply (clarsimp simp: parentOf_def mdb_next_unfold n_dest new_dest_def n) apply (cases "mdbNext src_node = dest") apply (subgoal_tac "m \<turnstile> src \<leadsto> dest") apply simp apply (subst mdb_next_unfold) apply (simp add: src) apply (case_tac "isUntypedCap src_cap") apply (clarsimp simp: isCap_simps isMDBParentOf_CTE is_derived'_def
    badge_derived'_def freeIndex_update_def capMasterCap_def split:capability.splits) apply (simp add: ut_revocable'_def) apply (drule spec[where x=src], simp add: isCap_simps) apply (simp add: descendants_of'_def) apply (drule spec[where x="mdbNext src_node"]) apply (erule notE, rule direct_parent) apply (simp add: mdb_next_unfold) apply simp apply (simp add: parentOf_def src isMDBParentOf_CTE isCap_simps cong:sameRegionAs_update_untyped) apply (clarsimp simp: isMDBParentOf_CTE is_derived'_def
    badge_derived'_def) apply (drule(2) revokable_plus_orderD) apply (erule sameRegionAsE, simp_all) apply (simp add: valid_badges_def2) apply (erule_tac x=src in allE) apply (erule_tac x="mdbNext src_node" in allE) apply (clarsimp simp: src mdb_next_unfold) apply (case_tac "capBadge cap'", simp_all) apply (clarsimp simp add: isCap_simps capMasterCap_def vsCapRef_def
                   simp del: not_ex
                      split: capability.splits) apply (clarsimp simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> dest \<rightarrow> p = False proof (prove)
using this:
m src = Some (CTE src_cap src_node)
is_derived' m src c' src_cap
valid_badges m
ut_revocable' m

goal (1 subgoal):
 1. n \<turnstile> dest \<rightarrow> p = False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; n \<turnstile> dest \<rightarrow> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c'a. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; n \<turnstile> dest \<leadsto> c'a; c'a \<noteq> 0; n \<turnstile> dest parentOf c'a\<rbrakk> \<Longrightarrow> False
 2. \<And>c'a c''. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; n \<turnstile> dest \<rightarrow> c'a; False; n \<turnstile> c'a \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c'a c''. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; n \<turnstile> dest \<rightarrow> c'a; False; n \<turnstile> c'a \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> False
 2. \<And>c'a. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; n \<turnstile> dest \<leadsto> c'a; c'a \<noteq> 0; n \<turnstile> dest parentOf c'a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c'a. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; n \<turnstile> dest \<leadsto> c'a; c'a \<noteq> 0; n \<turnstile> dest parentOf c'a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest; m \<turnstile> src \<leadsto> dest\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> dest
 3. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> dest
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> \<exists>z. m src = Some z \<and> dest = mdbNext (cteMDBNode z)
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; descendants_of' src m = {}; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104)\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; \<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; descendants_of' src m = {}; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104)\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; descendants_of' src m = {}; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; \<forall>x. \<not> m \<turnstile> src \<rightarrow> x; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node; \<not> m \<turnstile> src \<rightarrow> mdbNext src_node\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 2. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 3. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext src_node
 4. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0
 2. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext src_node
 3. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x101 cap' x102 node' x103 x104 f. \<lbrakk>valid_badges m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; m src = Some (CTE (capability.UntypedCap x101 x102 x103 f) src_node); global.sameRegionAs (capability.UntypedCap x101 x102 x103 x104) cap'; revokable' (capability.UntypedCap x101 x102 x103 f) (capability.UntypedCap x101 x102 x103 x104); c' = capability.UntypedCap x101 x102 x103 x104; src_cap = capability.UntypedCap x101 x102 x103 f; vsCapRef (capability.UntypedCap x101 x102 x103 f) = vsCapRef (capability.UntypedCap x101 x102 x103 x104); mdbRevocable src_node\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf mdbNext src_node
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_derived' m src c' src_cap; valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; global.sameRegionAs c' cap'; \<not> isIRQControlCap c'; revokable' src_cap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; global.sameRegionAs c' cap'; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isUntypedCap c' \<or> (\<exists>x. capBadge src_cap = Some 0 \<and> capBadge c' = Some x \<and> x \<noteq> 0)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap cap'; (Some 0, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capMasterCap c' = capMasterCap cap'; \<not> isZombie c'; \<not> isUntypedCap c'; \<not> isArchPageCap c'\<rbrakk> \<Longrightarrow> False
 2. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isUntypedCap c'\<rbrakk> \<Longrightarrow> False
 3. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isUntypedCap c' \<or> capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isArchPageCap c'; isArchPageCap cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); \<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'); ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap cap'; (Some 0, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capMasterCap c' = capMasterCap cap'; \<not> isZombie c'; \<not> isUntypedCap c'; \<not> isArchPageCap c'\<rbrakk> \<Longrightarrow> False
 2. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isUntypedCap c'\<rbrakk> \<Longrightarrow> False
 3. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isUntypedCap c' \<or> capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isArchPageCap c'; isArchPageCap cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap cap'; (Some 0, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capMasterCap c' = capMasterCap cap'; \<not> isZombie c'; \<not> isUntypedCap c'; \<not> isArchPageCap c'; \<forall>p' cap. (\<exists>node. m src = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> src \<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>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isUntypedCap c'\<rbrakk> \<Longrightarrow> False
 3. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isUntypedCap c' \<or> capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isArchPageCap c'; isArchPageCap cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap cap'; (Some 0, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capMasterCap c' = capMasterCap cap'; \<not> isZombie c'; \<not> isUntypedCap c'; \<not> isArchPageCap c'; \<forall>cap. (\<exists>node. m src = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m (mdbNext src_node) = Some (CTE cap' node') \<longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_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>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isUntypedCap c'\<rbrakk> \<Longrightarrow> False
 3. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isUntypedCap c' \<or> capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isArchPageCap c'; isArchPageCap cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cap' node' x. \<lbrakk>ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (Some x, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap cap'; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capMasterCap c' = capMasterCap cap'; \<not> isZombie c'; \<not> isUntypedCap c'; \<not> isArchPageCap c'; Some 0 \<noteq> capBadge cap' \<longrightarrow> mdbFirstBadged node'; capBadge src_cap = Some 0; capBadge c' = Some x; x \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isUntypedCap c'\<rbrakk> \<Longrightarrow> False
 3. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isUntypedCap c' \<or> capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isArchPageCap c'; isArchPageCap cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isUntypedCap c'\<rbrakk> \<Longrightarrow> False
 2. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isUntypedCap c' \<or> capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isArchPageCap c'; isArchPageCap cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); valid_badges m; ut_revocable' m; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; \<not> isUntypedCap src_cap; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap ARM_H.isPageCap c'; isArchCap ARM_H.isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap ARM_H.isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isUntypedCap c' \<or> capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange c'; isArchPageCap c'; isArchPageCap cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!