theory CNodeInv_R

lemma (in mdb_swap) cteSwap_valid_badges:
  "valid_badges n" proof - from valid have "valid_badges m" .. thus ?thesis using src dest apply (clarsimp simp add: valid_badges_def next_m_n2) apply (frule_tac p=p in n_cap) apply (frule_tac p=p' in n_cap) apply (drule badge_n)+ apply (clarsimp simp: s_d_swap_def sameRegion_ntfn sameRegion_ep
                          ep_simps region_simps
                    split: if_split_asm) apply fastforce apply fastforce apply fastforce 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_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_badges m proof (state)
this:
valid_badges m

goal (1 subgoal):
 1. valid_badges n proof (prove)
using this:
valid_badges m

goal (1 subgoal):
 1. valid_badges n proof (prove)
using this:
valid_badges m
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. valid_badges n proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n p = Some (CTE cap node); n p' = Some (CTE cap' node'); m \<turnstile> s_d_swap p src dest \<leadsto> s_d_swap p' src dest; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n p = Some (CTE cap node); n p' = Some (CTE cap' node'); m \<turnstile> s_d_swap p src dest \<leadsto> s_d_swap p' src dest; global.sameRegionAs cap cap'; if p = src then cap = dcap else if p = dest then cap = scap else \<exists>node'. m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n p = Some (CTE cap node); n p' = Some (CTE cap' node'); m \<turnstile> s_d_swap p src dest \<leadsto> s_d_swap p' src dest; global.sameRegionAs cap cap'; if p = src then cap = dcap else if p = dest then cap = scap else \<exists>node'. m p = Some (CTE cap node'); if p' = src then cap' = dcap else if p' = dest then cap' = scap else \<exists>node'. m p' = Some (CTE cap' node')\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m \<turnstile> s_d_swap p src dest \<leadsto> s_d_swap p' src dest; global.sameRegionAs cap cap'; if p = src then cap = dcap else if p = dest then cap = scap else \<exists>node'. m p = Some (CTE cap node'); if p' = src then cap' = dcap else if p' = dest then cap' = scap else \<exists>node'. m p' = Some (CTE cap' node'); if p = src then mdbFirstBadged node = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged node = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node'; if p' = src then mdbFirstBadged node' = mdbFirstBadged dest_node else if p' = dest then mdbFirstBadged node' = mdbFirstBadged src_node else \<exists>cap' node'a. m p' = Some (CTE cap' node'a) \<and> mdbFirstBadged node' = mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (4 subgoals):
 1. \<And>node node'. \<lbrakk>mdbFirstBadged node' = mdbFirstBadged dest_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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m \<turnstile> src \<leadsto> dest; global.sameRegionAs src_cap dest_cap; mdbFirstBadged node = mdbFirstBadged src_node\<rbrakk> \<Longrightarrow> (isEndpointCap src_cap \<longrightarrow> capEPBadge src_cap \<noteq> capEPBadge dest_cap \<longrightarrow> capEPBadge dest_cap \<noteq> 0 \<longrightarrow> mdbFirstBadged dest_node) \<and> (isNotificationCap src_cap \<longrightarrow> capNtfnBadge src_cap \<noteq> capNtfnBadge dest_cap \<longrightarrow> capNtfnBadge dest_cap \<noteq> 0 \<longrightarrow> mdbFirstBadged dest_node)
 2. \<And>node node'. \<lbrakk>mdbFirstBadged node = mdbFirstBadged dest_node; mdbFirstBadged node' = mdbFirstBadged 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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m \<turnstile> dest \<leadsto> src; global.sameRegionAs dest_cap src_cap\<rbrakk> \<Longrightarrow> (isEndpointCap dest_cap \<longrightarrow> capEPBadge dest_cap \<noteq> capEPBadge src_cap \<longrightarrow> capEPBadge src_cap \<noteq> 0 \<longrightarrow> mdbFirstBadged src_node) \<and> (isNotificationCap dest_cap \<longrightarrow> capNtfnBadge dest_cap \<noteq> capNtfnBadge src_cap \<longrightarrow> capNtfnBadge src_cap \<noteq> 0 \<longrightarrow> mdbFirstBadged src_node)
 3. \<And>p' node cap' node' node'a. \<lbrakk>mdbFirstBadged node = mdbFirstBadged dest_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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p' \<noteq> src; m \<turnstile> dest \<leadsto> p'; global.sameRegionAs dest_cap cap'; p' \<noteq> dest; m p' = Some (CTE cap' node'a); mdbFirstBadged node' = mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> (isEndpointCap dest_cap \<longrightarrow> capEPBadge dest_cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) \<and> (isNotificationCap dest_cap \<longrightarrow> capNtfnBadge dest_cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a)
 4. \<And>p' node cap' node' node'a. \<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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p' \<noteq> src; m \<turnstile> src \<leadsto> p'; global.sameRegionAs src_cap cap'; p' \<noteq> dest; m p' = Some (CTE cap' node'a); mdbFirstBadged node' = mdbFirstBadged node'a; mdbFirstBadged node = mdbFirstBadged src_node\<rbrakk> \<Longrightarrow> (isEndpointCap src_cap \<longrightarrow> capEPBadge src_cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) \<and> (isNotificationCap src_cap \<longrightarrow> capNtfnBadge src_cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) proof (prove)
goal (3 subgoals):
 1. \<And>node node'. \<lbrakk>mdbFirstBadged node = mdbFirstBadged dest_node; mdbFirstBadged node' = mdbFirstBadged 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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m \<turnstile> dest \<leadsto> src; global.sameRegionAs dest_cap src_cap\<rbrakk> \<Longrightarrow> (isEndpointCap dest_cap \<longrightarrow> capEPBadge dest_cap \<noteq> capEPBadge src_cap \<longrightarrow> capEPBadge src_cap \<noteq> 0 \<longrightarrow> mdbFirstBadged src_node) \<and> (isNotificationCap dest_cap \<longrightarrow> capNtfnBadge dest_cap \<noteq> capNtfnBadge src_cap \<longrightarrow> capNtfnBadge src_cap \<noteq> 0 \<longrightarrow> mdbFirstBadged src_node)
 2. \<And>p' node cap' node' node'a. \<lbrakk>mdbFirstBadged node = mdbFirstBadged dest_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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p' \<noteq> src; m \<turnstile> dest \<leadsto> p'; global.sameRegionAs dest_cap cap'; p' \<noteq> dest; m p' = Some (CTE cap' node'a); mdbFirstBadged node' = mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> (isEndpointCap dest_cap \<longrightarrow> capEPBadge dest_cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) \<and> (isNotificationCap dest_cap \<longrightarrow> capNtfnBadge dest_cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a)
 3. \<And>p' node cap' node' node'a. \<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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p' \<noteq> src; m \<turnstile> src \<leadsto> p'; global.sameRegionAs src_cap cap'; p' \<noteq> dest; m p' = Some (CTE cap' node'a); mdbFirstBadged node' = mdbFirstBadged node'a; mdbFirstBadged node = mdbFirstBadged src_node\<rbrakk> \<Longrightarrow> (isEndpointCap src_cap \<longrightarrow> capEPBadge src_cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) \<and> (isNotificationCap src_cap \<longrightarrow> capNtfnBadge src_cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) proof (prove)
goal (2 subgoals):
 1. \<And>p' node cap' node' node'a. \<lbrakk>mdbFirstBadged node = mdbFirstBadged dest_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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p' \<noteq> src; m \<turnstile> dest \<leadsto> p'; global.sameRegionAs dest_cap cap'; p' \<noteq> dest; m p' = Some (CTE cap' node'a); mdbFirstBadged node' = mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> (isEndpointCap dest_cap \<longrightarrow> capEPBadge dest_cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) \<and> (isNotificationCap dest_cap \<longrightarrow> capNtfnBadge dest_cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a)
 2. \<And>p' node cap' node' node'a. \<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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p' \<noteq> src; m \<turnstile> src \<leadsto> p'; global.sameRegionAs src_cap cap'; p' \<noteq> dest; m p' = Some (CTE cap' node'a); mdbFirstBadged node' = mdbFirstBadged node'a; mdbFirstBadged node = mdbFirstBadged src_node\<rbrakk> \<Longrightarrow> (isEndpointCap src_cap \<longrightarrow> capEPBadge src_cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) \<and> (isNotificationCap src_cap \<longrightarrow> capNtfnBadge src_cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) proof (prove)
goal (1 subgoal):
 1. \<And>p' node cap' node' node'a. \<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> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p' \<noteq> src; m \<turnstile> src \<leadsto> p'; global.sameRegionAs src_cap cap'; p' \<noteq> dest; m p' = Some (CTE cap' node'a); mdbFirstBadged node' = mdbFirstBadged node'a; mdbFirstBadged node = mdbFirstBadged src_node\<rbrakk> \<Longrightarrow> (isEndpointCap src_cap \<longrightarrow> capEPBadge src_cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) \<and> (isNotificationCap src_cap \<longrightarrow> capNtfnBadge src_cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'a) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_badges n

goal:
No subgoals!