theory CSpace1_R

lemma parent_of_m_n:
  "m \<turnstile> p parentOf c =
   n \<turnstile> s_d_swp p parentOf s_d_swp c" apply (clarsimp simp add: parentOf_def) apply (rule iffI) apply clarsimp apply (case_tac cte, case_tac cte') apply (rename_tac cap0 node0 cap1 node1) apply clarsimp apply (subgoal_tac "\<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')") prefer 2 apply (simp add: s_d_swap_def) apply (fastforce intro: n_exists) apply (subgoal_tac "\<exists>cap1' node1'. n (s_d_swap p src dest) = Some (CTE cap1' node1')") prefer 2 apply (simp add: s_d_swap_def) apply (fastforce intro: n_exists) apply clarsimp apply (insert src_derived dest_derived)[1] apply (erule isMDBParentOf_eq) apply simp apply (drule n_cap)+ subgoal by (simp add: s_d_swap_def src dest split: if_split_asm) apply simp apply (drule revokable)+ subgoal by (simp add: s_d_swap_def src dest split: if_split_asm) apply simp apply (drule n_cap)+ subgoal by (simp add: s_d_swap_def src dest split: if_split_asm) apply simp apply (drule badge_n)+ subgoal by (simp add: s_d_swap_def src dest split: if_split_asm) apply clarsimp apply (case_tac cte, case_tac cte') apply (rename_tac cap0 node0 cap1 node1) apply clarsimp apply (subgoal_tac "\<exists>cap0' node0' cap1' node1'.
                      m c = Some (CTE cap0' node0') \<and>
                      m p = Some (CTE cap1' node1')") prefer 2 apply (drule m_exists)+ apply clarsimp apply (simp add: s_d_swap_def src dest split: if_split_asm) apply clarsimp apply (insert src_derived dest_derived)[1] apply (erule isMDBParentOf_eq) apply simp apply (rule weak_derived_sym') apply (drule n_cap)+ apply (simp add: s_d_swap_def src dest split: if_split_asm) apply simp apply (drule revokable)+ subgoal by (simp add: s_d_swap_def src dest split: if_split_asm) apply simp apply (rule weak_derived_sym') apply (drule n_cap)+ subgoal by (simp add: s_d_swap_def src dest split: if_split_asm) apply simp apply (drule badge_n)+ subgoal by (simp add: s_d_swap_def src dest split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p parentOf c = n \<turnstile> s_d_swp p parentOf s_d_swp c proof (prove)
goal (1 subgoal):
 1. (\<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte) = (\<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte) proof (prove)
goal (2 subgoals):
 1. \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>m c = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>m c = Some cte; m p = Some cte'; isMDBParentOf cte' cte; cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte cap0 node0 cap1 node1. \<lbrakk>m c = Some cte; m p = Some cte'; isMDBParentOf cte' cte; cte = CTE cap0 node0; cte' = CTE cap1 node1\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0)\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0)\<rbrakk> \<Longrightarrow> \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0)\<rbrakk> \<Longrightarrow> \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0)\<rbrakk> \<Longrightarrow> (c = dest \<longrightarrow> (\<exists>cap0' node0'. n src = Some (CTE cap0' node0'))) \<and> (c \<noteq> dest \<longrightarrow> (c = src \<longrightarrow> (\<exists>cap0' node0'. n dest = Some (CTE cap0' node0'))) \<and> (c \<noteq> src \<longrightarrow> (\<exists>cap0' node0'. n c = Some (CTE cap0' node0'))))
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0'); \<exists>cap1' node1'. n (s_d_swap p src dest) = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')\<rbrakk> \<Longrightarrow> \<exists>cap1' node1'. n (s_d_swap p src dest) = Some (CTE cap1' node1')
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0')\<rbrakk> \<Longrightarrow> \<exists>cap1' node1'. n (s_d_swap p src dest) = Some (CTE cap1' node1')
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0'); \<exists>cap1' node1'. n (s_d_swap p src dest) = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (if c = src then dest else if c = dest then src else c) = Some (CTE cap0' node0')\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> (\<exists>cap1' node1'. n src = Some (CTE cap1' node1'))) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (\<exists>cap1' node1'. n dest = Some (CTE cap1' node1'))) \<and> (p \<noteq> src \<longrightarrow> (\<exists>cap1' node1'. n p = Some (CTE cap1' node1'))))
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0'); \<exists>cap1' node1'. n (s_d_swap p src dest) = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0'. n (s_d_swap c src dest) = Some (CTE cap0' node0'); \<exists>cap1' node1'. n (s_d_swap p src dest) = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap1' node1') (CTE cap0' node0')
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap1' node1') (CTE cap0' node0')
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (5 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap1 node1)) (cteCap (CTE cap1' node1'))
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 4. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 5. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (5 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' cap1 cap1'
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 4. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 5. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (5 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then cap0' = dcap else if s_d_swap c src dest = dest then cap0' = scap else \<exists>node'. m (s_d_swap c src dest) = Some (CTE cap0' node'); if s_d_swap p src dest = src then cap1' = dcap else if s_d_swap p src dest = dest then cap1' = scap else \<exists>node'. m (s_d_swap p src dest) = Some (CTE cap1' node')\<rbrakk> \<Longrightarrow> weak_derived' cap1 cap1'
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 4. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 5. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some (CTE cap0_ node0_); m p = Some (CTE cap1_ node1_); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then cap0'_ = dcap else if s_d_swap c src dest = dest then cap0'_ = scap else \<exists>node'. m (s_d_swap c src dest) = Some (CTE cap0'_ node'); if s_d_swap p src dest = src then cap1'_ = dcap else if s_d_swap p src dest = dest then cap1'_ = scap else \<exists>node'. m (s_d_swap p src dest) = Some (CTE cap1'_ node')\<rbrakk> \<Longrightarrow> weak_derived' cap1_ cap1'_ proof (prove)
goal (4 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 4. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (4 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable node1' = mdbRevocable node1
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 4. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (4 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then mdbRevocable node0' = mdbRevocable dest_node else if s_d_swap c src dest = dest then mdbRevocable node0' = mdbRevocable src_node else \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node') \<and> mdbRevocable node0' = mdbRevocable node'; if s_d_swap p src dest = src then mdbRevocable node1' = mdbRevocable dest_node else if s_d_swap p src dest = dest then mdbRevocable node1' = mdbRevocable src_node else \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node') \<and> mdbRevocable node1' = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node1' = mdbRevocable node1
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 4. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some (CTE cap0_ node0_); m p = Some (CTE cap1_ node1_); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then mdbRevocable node0'_ = mdbRevocable dest_node else if s_d_swap c src dest = dest then mdbRevocable node0'_ = mdbRevocable src_node else \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node') \<and> mdbRevocable node0'_ = mdbRevocable node'; if s_d_swap p src dest = src then mdbRevocable node1'_ = mdbRevocable dest_node else if s_d_swap p src dest = dest then mdbRevocable node1'_ = mdbRevocable src_node else \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node') \<and> mdbRevocable node1'_ = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node1'_ = mdbRevocable node1_ proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' cap0 cap0'
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then cap0' = dcap else if s_d_swap c src dest = dest then cap0' = scap else \<exists>node'. m (s_d_swap c src dest) = Some (CTE cap0' node'); if s_d_swap p src dest = src then cap1' = dcap else if s_d_swap p src dest = dest then cap1' = scap else \<exists>node'. m (s_d_swap p src dest) = Some (CTE cap1' node')\<rbrakk> \<Longrightarrow> weak_derived' cap0 cap0'
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 3. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some (CTE cap0_ node0_); m p = Some (CTE cap1_ node1_); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then cap0'_ = dcap else if s_d_swap c src dest = dest then cap0'_ = scap else \<exists>node'. m (s_d_swap c src dest) = Some (CTE cap0'_ node'); if s_d_swap p src dest = src then cap1'_ = dcap else if s_d_swap p src dest = dest then cap1'_ = scap else \<exists>node'. m (s_d_swap p src dest) = Some (CTE cap1'_ node')\<rbrakk> \<Longrightarrow> weak_derived' cap0_ cap0'_ proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0))
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); n (s_d_swap c src dest) = Some (CTE cap0' node0'); n (s_d_swap p src dest) = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged node0' = mdbFirstBadged node0
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0 node0); m p = Some (CTE cap1 node1); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then mdbFirstBadged node0' = mdbFirstBadged dest_node else if s_d_swap c src dest = dest then mdbFirstBadged node0' = mdbFirstBadged src_node else \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node') \<and> mdbFirstBadged node0' = mdbFirstBadged node'; if s_d_swap p src dest = src then mdbFirstBadged node1' = mdbFirstBadged dest_node else if s_d_swap p src dest = dest then mdbFirstBadged node1' = mdbFirstBadged src_node else \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node') \<and> mdbFirstBadged node1' = mdbFirstBadged node'\<rbrakk> \<Longrightarrow> mdbFirstBadged node0' = mdbFirstBadged node0
 2. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some (CTE cap0_ node0_); m p = Some (CTE cap1_ node1_); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then mdbFirstBadged node0'_ = mdbFirstBadged dest_node else if s_d_swap c src dest = dest then mdbFirstBadged node0'_ = mdbFirstBadged src_node else \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node') \<and> mdbFirstBadged node0'_ = mdbFirstBadged node'; if s_d_swap p src dest = src then mdbFirstBadged node1'_ = mdbFirstBadged dest_node else if s_d_swap p src dest = dest then mdbFirstBadged node1'_ = mdbFirstBadged src_node else \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node') \<and> mdbFirstBadged node1'_ = mdbFirstBadged node'\<rbrakk> \<Longrightarrow> mdbFirstBadged node0'_ = mdbFirstBadged node0_ proof (prove)
goal (1 subgoal):
 1. \<exists>cte' cte. n (s_d_swap c src dest) = Some cte \<and> n (s_d_swap p src dest) = Some cte' \<and> isMDBParentOf cte' cte \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>n (s_d_swap c src dest) = Some cte; n (s_d_swap p src dest) = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>n (s_d_swap c src dest) = Some cte; n (s_d_swap p src dest) = Some cte'; isMDBParentOf cte' cte; cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some cte; n (s_d_swap p src dest) = Some cte'; isMDBParentOf cte' cte; cte = CTE cap0 node0; cte' = CTE cap1 node1\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0)\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0' cap1' node1'. m c = Some (CTE cap0' node0') \<and> m p = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0)\<rbrakk> \<Longrightarrow> \<exists>cap0' node0' cap1' node1'. m c = Some (CTE cap0' node0') \<and> m p = Some (CTE cap1' node1') proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0)\<rbrakk> \<Longrightarrow> \<exists>cap0' node0' cap1' node1'. m c = Some (CTE cap0' node0') \<and> m p = Some (CTE cap1' node1')
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0' cap1' node1'. m c = Some (CTE cap0' node0') \<and> m p = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node'); \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node')\<rbrakk> \<Longrightarrow> \<exists>cap0' node0' cap1' node1'. m c = Some (CTE cap0' node0') \<and> m p = Some (CTE cap1' node1')
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0' cap1' node1'. m c = Some (CTE cap0' node0') \<and> m p = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap' cap'a node' node'a. \<lbrakk>isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); m (s_d_swap c src dest) = Some (CTE cap' node'); m (s_d_swap p src dest) = Some (CTE cap'a node'a)\<rbrakk> \<Longrightarrow> (\<exists>cap0' node0'. m c = Some (CTE cap0' node0')) \<and> (\<exists>cap1' node1'. m p = Some (CTE cap1' node1'))
 2. \<And>cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0' cap1' node1'. m c = Some (CTE cap0' node0') \<and> m p = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cap0 node0 cap1 node1. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); \<exists>cap0' node0' cap1' node1'. m c = Some (CTE cap0' node0') \<and> m p = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m c = Some cte \<and> m p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1')\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap1' node1') (CTE cap0' node0') proof (prove)
goal (1 subgoal):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); isMDBParentOf (CTE cap1 node1) (CTE cap0 node0); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap1' node1') (CTE cap0' node0') proof (prove)
goal (4 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap1 node1)) (cteCap (CTE cap1' node1'))
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 4. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (4 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' cap1 cap1'
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 4. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (4 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' cap1' cap1
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 4. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (4 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then cap0 = dcap else if s_d_swap c src dest = dest then cap0 = scap else \<exists>node'. m (s_d_swap c src dest) = Some (CTE cap0 node'); if s_d_swap p src dest = src then cap1 = dcap else if s_d_swap p src dest = dest then cap1 = scap else \<exists>node'. m (s_d_swap p src dest) = Some (CTE cap1 node')\<rbrakk> \<Longrightarrow> weak_derived' cap1' cap1
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 4. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode (CTE cap1' node1')) = mdbRevocable (cteMDBNode (CTE cap1 node1))
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbRevocable node1' = mdbRevocable node1
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (3 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then mdbRevocable node0 = mdbRevocable dest_node else if s_d_swap c src dest = dest then mdbRevocable node0 = mdbRevocable src_node else \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node') \<and> mdbRevocable node0 = mdbRevocable node'; if s_d_swap p src dest = src then mdbRevocable node1 = mdbRevocable dest_node else if s_d_swap p src dest = dest then mdbRevocable node1 = mdbRevocable src_node else \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node') \<and> mdbRevocable node1 = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node1' = mdbRevocable node1
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 3. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some (CTE cap0'_ node0'_); m p = Some (CTE cap1'_ node1'_); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then mdbRevocable node0_ = mdbRevocable dest_node else if s_d_swap c src dest = dest then mdbRevocable node0_ = mdbRevocable src_node else \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node') \<and> mdbRevocable node0_ = mdbRevocable node'; if s_d_swap p src dest = src then mdbRevocable node1_ = mdbRevocable dest_node else if s_d_swap p src dest = dest then mdbRevocable node1_ = mdbRevocable src_node else \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node') \<and> mdbRevocable node1_ = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node1'_ = mdbRevocable node1_ proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' (cteCap (CTE cap0 node0)) (cteCap (CTE cap0' node0'))
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' cap0 cap0'
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> weak_derived' cap0' cap0
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (2 subgoals):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then cap0 = dcap else if s_d_swap c src dest = dest then cap0 = scap else \<exists>node'. m (s_d_swap c src dest) = Some (CTE cap0 node'); if s_d_swap p src dest = src then cap1 = dcap else if s_d_swap p src dest = dest then cap1 = scap else \<exists>node'. m (s_d_swap p src dest) = Some (CTE cap1 node')\<rbrakk> \<Longrightarrow> weak_derived' cap0' cap0
 2. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some (CTE cap0'_ node0'_); m p = Some (CTE cap1'_ node1'_); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then cap0_ = dcap else if s_d_swap c src dest = dest then cap0_ = scap else \<exists>node'. m (s_d_swap c src dest) = Some (CTE cap0_ node'); if s_d_swap p src dest = src then cap1_ = dcap else if s_d_swap p src dest = dest then cap1_ = scap else \<exists>node'. m (s_d_swap p src dest) = Some (CTE cap1_ node')\<rbrakk> \<Longrightarrow> weak_derived' cap0'_ cap0_ proof (prove)
goal (1 subgoal):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode (CTE cap0' node0')) = mdbFirstBadged (cteMDBNode (CTE cap0 node0)) proof (prove)
goal (1 subgoal):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>n (s_d_swap c src dest) = Some (CTE cap0 node0); n (s_d_swap p src dest) = Some (CTE cap1 node1); m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap\<rbrakk> \<Longrightarrow> mdbFirstBadged node0' = mdbFirstBadged node0 proof (prove)
goal (1 subgoal):
 1. \<And>cap0 node0 cap1 node1 cap0' cap1' node0' node1'. \<lbrakk>m c = Some (CTE cap0' node0'); m p = Some (CTE cap1' node1'); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then mdbFirstBadged node0 = mdbFirstBadged dest_node else if s_d_swap c src dest = dest then mdbFirstBadged node0 = mdbFirstBadged src_node else \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node') \<and> mdbFirstBadged node0 = mdbFirstBadged node'; if s_d_swap p src dest = src then mdbFirstBadged node1 = mdbFirstBadged dest_node else if s_d_swap p src dest = dest then mdbFirstBadged node1 = mdbFirstBadged src_node else \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node') \<and> mdbFirstBadged node1 = mdbFirstBadged node'\<rbrakk> \<Longrightarrow> mdbFirstBadged node0' = mdbFirstBadged node0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some (CTE cap0'_ node0'_); m p = Some (CTE cap1'_ node1'_); weak_derived' src_cap scap; weak_derived' dest_cap dcap; if s_d_swap c src dest = src then mdbFirstBadged node0_ = mdbFirstBadged dest_node else if s_d_swap c src dest = dest then mdbFirstBadged node0_ = mdbFirstBadged src_node else \<exists>cap' node'. m (s_d_swap c src dest) = Some (CTE cap' node') \<and> mdbFirstBadged node0_ = mdbFirstBadged node'; if s_d_swap p src dest = src then mdbFirstBadged node1_ = mdbFirstBadged dest_node else if s_d_swap p src dest = dest then mdbFirstBadged node1_ = mdbFirstBadged src_node else \<exists>cap' node'. m (s_d_swap p src dest) = Some (CTE cap' node') \<and> mdbFirstBadged node1_ = mdbFirstBadged node'\<rbrakk> \<Longrightarrow> mdbFirstBadged node0'_ = mdbFirstBadged node0_ proof (prove)
goal:
No subgoals!