theory CSpace1_R

lemma parent_preserved:
  "isMDBParentOf cte (CTE src_cap src_node) \<Longrightarrow> isMDBParentOf cte new_dest" using partial_is_derived' apply (cases cte) apply (case_tac "isUntypedCap src_cap") apply (clarsimp simp:isCap_simps isMDBParentOf_CTE freeIndex_update_def new_dest_def) apply (clarsimp simp:is_derived'_def isCap_simps badge_derived'_def capMasterCap_def split:capability.splits) apply (clarsimp simp:sameRegionAs_def2 capMasterCap_def isCap_simps split:capability.splits) apply (clarsimp simp: isMDBParentOf_CTE) apply (clarsimp simp: new_dest_def) apply (rename_tac cap node) apply (clarsimp simp: is_derived'_def badge_derived'_def) apply (rule conjI) apply (simp add: sameRegionAs_def2) apply (cases "revokable' src_cap c'") apply simp apply (drule(2) revokable_plus_orderD) apply (erule disjE) apply (clarsimp simp: isCap_simps) apply (fastforce elim: capBadge_ordering_trans)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf cte (CTE src_cap src_node) \<Longrightarrow> isMDBParentOf cte new_dest proof (prove)
using this:
is_derived' m src c' src_cap

goal (1 subgoal):
 1. isMDBParentOf cte (CTE src_cap src_node) \<Longrightarrow> isMDBParentOf cte new_dest proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>isMDBParentOf cte (CTE src_cap src_node); is_derived' m src c' src_cap; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte new_dest proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>isMDBParentOf cte (CTE src_cap src_node); is_derived' m src c' src_cap; cte = CTE x1 x2; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> isMDBParentOf cte new_dest
 2. \<And>x1 x2. \<lbrakk>isMDBParentOf cte (CTE src_cap src_node); is_derived' m src c' src_cap; cte = CTE x1 x2; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> isMDBParentOf cte new_dest proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 d v0 v1 f. \<lbrakk>is_derived' m src c' (capability.UntypedCap d v0 v1 f); cte = CTE x1 x2; src_cap = capability.UntypedCap d v0 v1 f; global.sameRegionAs x1 (capability.UntypedCap d v0 v1 f); mdbRevocable x2; capBadge x1 = None\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 c'
 2. \<And>x1 x2. \<lbrakk>isMDBParentOf cte (CTE src_cap src_node); is_derived' m src c' src_cap; cte = CTE x1 x2; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> isMDBParentOf cte new_dest proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 d v0 v1 f x104. \<lbrakk>cte = CTE x1 x2; src_cap = capability.UntypedCap d v0 v1 f; global.sameRegionAs x1 (capability.UntypedCap d v0 v1 f); mdbRevocable x2; capBadge x1 = None; c' = capability.UntypedCap d v0 v1 x104; descendants_of' src m = {}; vsCapRef (capability.UntypedCap d v0 v1 f) = vsCapRef (capability.UntypedCap d v0 v1 x104)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 (capability.UntypedCap d v0 v1 x104)
 2. \<And>x1 x2. \<lbrakk>isMDBParentOf cte (CTE src_cap src_node); is_derived' m src c' src_cap; cte = CTE x1 x2; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> isMDBParentOf cte new_dest proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>isMDBParentOf cte (CTE src_cap src_node); is_derived' m src c' src_cap; cte = CTE x1 x2; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> isMDBParentOf cte new_dest proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>is_derived' m src c' src_cap; cte = CTE x1 x2; \<not> isUntypedCap src_cap; global.sameRegionAs x1 src_cap; mdbRevocable x2; (capBadge x1, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node)\<rbrakk> \<Longrightarrow> \<exists>cap' node'. new_dest = CTE cap' node' \<and> global.sameRegionAs x1 cap' \<and> (capBadge x1, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>is_derived' m src c' src_cap; cte = CTE x1 x2; \<not> isUntypedCap src_cap; global.sameRegionAs x1 src_cap; mdbRevocable x2; (capBadge x1, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 c' \<and> (capBadge x1, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (1 subgoal):
 1. \<And>cap node. \<lbrakk>is_derived' m src c' src_cap; cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap c' \<and> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (1 subgoal):
 1. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap c' \<and> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (2 subgoals):
 1. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap c'
 2. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y)\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (1 subgoal):
 1. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y)\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (2 subgoals):
 1. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); revokable' src_cap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c')
 2. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); \<not> revokable' src_cap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (2 subgoals):
 1. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); revokable' src_cap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering True
 2. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); \<not> revokable' src_cap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (2 subgoals):
 1. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap 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> (capBadge cap, capBadge c') \<in> capBadge_ordering True
 2. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); \<not> revokable' src_cap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (3 subgoals):
 1. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap 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); vsCapRef src_cap = vsCapRef c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering True
 2. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap 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); isArchCap isPageCap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering True
 3. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); \<not> revokable' src_cap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal (3 subgoals):
 1. \<And>cap node. \<lbrakk>cte = CTE cap node; \<forall>d v0 v1 f. src_cap \<noteq> capability.UntypedCap d v0 v1 f; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<forall>v0 v1 v2. src_cap \<noteq> capability.Zombie v0 v1 v2; c' \<noteq> capability.IRQControlCap; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; (\<exists>v0 v1 v2. src_cap = capability.ReplyCap v0 v1 v2) = (\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2); (\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> capReplyMaster src_cap; (\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> \<not> capReplyMaster c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); (\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<or> capBadge src_cap = Some 0 \<and> (\<exists>x. capBadge c' = Some x \<and> x \<noteq> 0); vsCapRef src_cap = vsCapRef c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering True
 2. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap 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); isArchCap isPageCap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering True
 3. \<And>cap node. \<lbrakk>cte = CTE cap node; \<not> isUntypedCap src_cap; global.sameRegionAs cap src_cap; mdbRevocable node; (capBadge cap, capBadge src_cap) \<in> capBadge_ordering (mdbFirstBadged src_node); c' \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isIRQControlCap c'; 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 isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); \<not> revokable' src_cap c'\<rbrakk> \<Longrightarrow> (capBadge cap, capBadge c') \<in> capBadge_ordering (revokable' src_cap c') proof (prove)
goal:
No subgoals!