theory CSpace_R

lemma cteInsert_valid_dlist:
  "\<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and
    (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and valid_objs' and
    (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace>
   cteInsert cap src dest
   \<lbrace>\<lambda>_ s. valid_dlist (ctes_of s) \<rbrace>" apply (rule hoare_name_pre_state) apply clarsimp apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: if_split) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of
        setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map getCTE_wp
        setUntypedCapAsFull_valid_dlist mdb_inv_preserve_fun_upd | simp)+ apply (intro conjI impI) apply (clarsimp simp:cte_wp_at_ctes_of) apply (intro conjI) apply (clarsimp simp:valid_mdb_ctes_def no_0_def)+ apply (frule mdb_chain_0_no_loops) apply (simp add:no_0_def) apply (rule valid_dlistI) apply (case_tac "p = dest") apply (clarsimp simp:modify_map_def nullPointer_def split:if_split_asm)+ apply (frule(2) valid_dlist_prevD) apply simp apply (subgoal_tac "mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)") prefer 2 apply (clarsimp) apply (drule(3) no_loops_no_l2_loop[rotated -1],simp) apply (subgoal_tac "mdbPrev (cteMDBNode ctea) \<noteq> dest") apply clarsimp+ apply (frule_tac p = p and m = "ctes_of sa" in valid_dlist_prevD) apply simp+ apply fastforce apply (case_tac "p = dest") apply (clarsimp simp:modify_map_def nullPointer_def split:if_split_asm)+ apply (frule(2) valid_dlist_nextD,clarsimp) apply (clarsimp simp:modify_map_def nullPointer_def split:if_split_asm) apply (frule(2) valid_dlist_nextD) apply simp apply (subgoal_tac "mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)") prefer 2 apply (clarsimp) apply (drule(3) no_loops_no_l2_loop[rotated -1],simp) apply clarsimp apply (intro conjI impI) apply clarsimp+ apply (drule_tac cte = cte' in no_loops_no_l2_loop,simp) apply simp+ apply (frule(2) valid_dlist_nextD) apply clarsimp apply (frule_tac p = p and m = "ctes_of sa" in valid_dlist_nextD) apply clarsimp+ apply (rule conjI) apply fastforce apply (intro conjI impI,clarsimp+) apply (frule_tac valid_dlist_nextD) apply clarsimp+ apply (frule_tac valid_dlist_nextD) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_ s. valid_dlist (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_ s. valid_dlist (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb' s; pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_ s. valid_dlist (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb' s; pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do srcCTE <- getCTE src;
srcMDB <- return (cteMDBNode srcCTE);
srcCap <- return (cteCap srcCTE);
newCapIsRevocable <- return (revokable' srcCap cap);
newMDB <- return (mdbFirstBadged_update (\<lambda>_. newCapIsRevocable) (mdbRevocable_update (\<lambda>_. newCapIsRevocable) (mdbPrev_update (\<lambda>_. src) srcMDB)));
oldCTE <- getCTE dest;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
setUntypedCapAsFull srcCap cap src;
do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
updateMDB dest (const newMDB);
updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext newMDB) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. valid_dlist (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. valid_dlist (ctes_of s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s srcCTE x y ya. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s srcCTE x y ya\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. \<forall>cte. cte_wp_at' ((=) cte) dest s \<longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) \<and> no_0 (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) \<and> no_0 (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) \<and> valid_dlist (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrace>
 2. \<And>s srcCTE x y. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B11 s srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B12 s srcCTE x y\<rbrace>
 3. \<And>s srcCTE x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B10 s srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B11 s srcCTE x\<rbrace>
 4. \<And>s srcCTE. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B9 s srcCTE\<rbrace> getCTE dest \<lbrace>?B10 s srcCTE\<rbrace>
 5. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s\<rbrace> getCTE src \<lbrace>?B9 s\<rbrace>
 6. \<And>s sa. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s; s = sa\<rbrakk> \<Longrightarrow> ?Q8 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s srcCTE x cte. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; ctes_of s src = Some cte; is_derived' (ctes_of s) src cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s srcCTE x () ()\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. \<forall>cte. ctes_of s dest = Some cte \<longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) \<and> valid_dlist (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrace>
 2. \<And>s srcCTE x y. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B11 s srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B12 s srcCTE x y\<rbrace>
 3. \<And>s srcCTE x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B10 s srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B11 s srcCTE x\<rbrace>
 4. \<And>s srcCTE. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B9 s srcCTE\<rbrace> getCTE dest \<lbrace>?B10 s srcCTE\<rbrace>
 5. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s\<rbrace> getCTE src \<lbrace>?B9 s\<rbrace>
 6. \<And>s sa. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s; s = sa\<rbrakk> \<Longrightarrow> ?Q8 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; cte_wp_at' (is_derived' (ctes_of sa) src cap \<circ> cteCap) src sa; s = sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src sa \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src sa) \<and> \<not> cte_wp_at' (\<lambda>_. True) dest sa \<or> (\<forall>x. \<exists>cte. cte_wp_at' ((=) cte) src sa \<and> (\<exists>ctea. cte_wp_at' ((=) ctea) dest sa \<and> (cteCap ctea = capability.NullCap \<longrightarrow> ctes_of sa dest = Some x \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) \<and> cte_wp_at' ((=) cte) src sa \<and> valid_dlist (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> cte_wp_at' (\<lambda>c. c = cte) src sa))) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; cte_wp_at' (is_derived' (ctes_of sa) src cap \<circ> cteCap) src sa; s = sa; cte_wp_at' (\<lambda>_. True) src sa\<rbrakk> \<Longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src sa) \<and> \<not> cte_wp_at' (\<lambda>_. True) dest sa \<or> (\<forall>x. \<exists>cte. cte_wp_at' ((=) cte) src sa \<and> (\<exists>ctea. cte_wp_at' ((=) ctea) dest sa \<and> (cteCap ctea = capability.NullCap \<longrightarrow> ctes_of sa dest = Some x \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) \<and> cte_wp_at' ((=) cte) src sa \<and> valid_dlist (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> cte_wp_at' (\<lambda>c. c = cte) src sa))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) \<and> valid_dlist (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a)
 2. \<And>sa ctea x. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer\<rbrakk> \<Longrightarrow> valid_dlist (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa)\<rbrakk> \<Longrightarrow> valid_dlist (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa)\<rbrakk> \<Longrightarrow> no_0 (ctes_of sa)
 2. \<And>sa ctea x. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa)\<rbrakk> \<Longrightarrow> valid_dlist (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa)\<rbrakk> \<Longrightarrow> valid_dlist (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; p = dest\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 3. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = src)) \<and> (mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src)))))
 2. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 3. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = src)) \<and> (mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src)))))
 2. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 3. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = src))))
 2. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 3. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (4 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = src))))
 2. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)
 3. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 4. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (4 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)
 2. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = src))))
 3. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 4. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (4 subgoals):
 1. \<And>sa ctea x cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; mdbNext (cteMDBNode cte') \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa (mdbNext (cteMDBNode cte')) = Some ctea; is_derived' (ctes_of sa) (mdbNext (cteMDBNode cte')) cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; src = mdbNext (cteMDBNode cte'); mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = src))))
 3. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 4. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = src))))
 2. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 3. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (4 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode ctea) \<noteq> dest\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest \<and> (mdbPrev (cteMDBNode ctea) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> src \<and> (mdbPrev (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = src))))
 2. \<And>sa ctea x. \<lbrakk>mdbPrev (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode ctea)) = Some cte' \<and> mdbNext (cteMDBNode cte') = src; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> dest
 3. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 4. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 2. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (4 subgoals):
 1. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> valid_dlist (ctes_of sa)
 2. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0
 3. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte; \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p))))))
 4. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x p cte. \<lbrakk>mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte; \<exists>cte'. ctes_of sa (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> dest \<and> (mdbPrev (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> src \<and> (mdbPrev (cteMDBNode cte) \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbNext (cteMDBNode cte') = p)))))
 2. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; p = dest\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p
 2. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); dest \<noteq> mdbNext (cteMDBNode ctea); mdbNext (cteMDBNode ctea) \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = dest
 2. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x p cte. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>cte'. modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap ctea) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode ctea)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode ctea)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest \<and> (mdbNext (cteMDBNode z) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode z) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)) \<and> (mdbNext (cteMDBNode z) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea) \<and> (mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea)))))
 2. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest \<and> (mdbNext (cteMDBNode z) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode z) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)) \<and> (mdbNext (cteMDBNode z) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea) \<and> (mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea)))))
 2. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest \<and> (mdbNext (cteMDBNode z) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode z) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)) \<and> (mdbNext (cteMDBNode z) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea)))
 2. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (4 subgoals):
 1. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest \<and> (mdbNext (cteMDBNode z) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode z) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)) \<and> (mdbNext (cteMDBNode z) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea)))
 2. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)
 3. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 4. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (4 subgoals):
 1. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)
 2. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest \<and> (mdbNext (cteMDBNode z) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode z) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)) \<and> (mdbNext (cteMDBNode z) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea)))
 3. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 4. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (4 subgoals):
 1. \<And>sa ctea x z cte'. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; ctes_of sa (mdbNext (cteMDBNode z)) = Some cte'; mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest \<and> (mdbNext (cteMDBNode z) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode z) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)) \<and> (mdbNext (cteMDBNode z) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea)))
 3. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 4. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode z)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest \<and> (mdbNext (cteMDBNode z) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode z) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbNext (cteMDBNode ctea)) \<and> (mdbNext (cteMDBNode z) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea)))
 2. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x z cte'. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); ctes_of sa (mdbNext (cteMDBNode z)) = Some cte'; mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest \<and> (mdbNext (cteMDBNode z) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> src \<and> (mdbNext (cteMDBNode z) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea)))
 2. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (5 subgoals):
 1. \<And>sa ctea x z cte'. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); ctes_of sa (mdbNext (cteMDBNode z)) = Some cte'; mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> dest
 2. \<And>sa ctea x z cte'. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); ctes_of sa (mdbNext (cteMDBNode z)) = Some cte'; mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbNext (cteMDBNode z) \<noteq> dest\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> src
 3. \<And>sa ctea x z cte'. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); ctes_of sa (mdbNext (cteMDBNode z)) = Some cte'; mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbNext (cteMDBNode z) \<noteq> dest; mdbNext (cteMDBNode z) \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> mdbNext (cteMDBNode ctea)
 4. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 5. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbNext (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 3. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (5 subgoals):
 1. \<And>sa ctea x cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbNext (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> ctes_of sa (?p509 sa ctea x cte') = Some cte'
 2. \<And>sa ctea x cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbNext (cteMDBNode cte') = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode cte')
 3. \<And>sa ctea x cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; mdbNext (cteMDBNode ctea) \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbNext (cteMDBNode ctea) \<noteq> src; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; mdbPrev (cteMDBNode ctea) \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbNext (cteMDBNode cte') = mdbNext (cteMDBNode ctea); mdbNext (cteMDBNode cte') = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 5. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False
 2. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa (mdbNext (cteMDBNode ctea)) = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); src \<noteq> mdbNext (cteMDBNode ctea); dest = mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> False
 2. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> valid_dlist (ctes_of sa)
 2. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0
 3. \<And>sa ctea x p cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); p \<noteq> mdbNext (cteMDBNode ctea); p \<noteq> src; ctes_of sa p = Some cte; \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = p) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte') \<and> mdbPrev (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'. ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbPrev (cteMDBNode cte'))) \<and> (mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbPrev (cteMDBNode cte')) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'a. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte'a) \<and> mdbPrev (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte')))))) proof (prove)
goal (2 subgoals):
 1. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode ctea) = dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbPrev (cteMDBNode cte'))
 2. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbPrev (cteMDBNode cte')) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'a. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte'a) \<and> mdbPrev (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte'))))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode ctea) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode ctea) = src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> src)) \<and> (mdbNext (cteMDBNode ctea) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest \<and> (mdbNext (cteMDBNode cte) \<noteq> dest \<longrightarrow> (mdbNext (cteMDBNode cte) = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = mdbPrev (cteMDBNode cte')) \<and> (mdbNext (cteMDBNode cte) \<noteq> src \<longrightarrow> mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea) \<longrightarrow> (\<exists>cte'a. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte'a) \<and> mdbPrev (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte'))))) proof (prove)
goal (4 subgoals):
 1. \<And>sa x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte') \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa (mdbNext (cteMDBNode cte')) = Some cte'; is_derived' (ctes_of sa) (mdbNext (cteMDBNode cte')) cap (cteCap cte'); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode cte'); ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; mdbNext (cteMDBNode cte') \<noteq> dest; src = mdbNext (cteMDBNode cte'); mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte')\<rbrakk> \<Longrightarrow> False
 2. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest
 3. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src; mdbNext (cteMDBNode cte) \<noteq> dest; mdbNext (cteMDBNode cte) = src\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode ctea) = mdbPrev (cteMDBNode cte')
 4. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src; mdbNext (cteMDBNode cte) \<noteq> dest; mdbNext (cteMDBNode cte) \<noteq> src; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> \<exists>cte'a. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte'a) \<and> mdbPrev (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte') proof (prove)
goal (6 subgoals):
 1. \<And>sa x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte') \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa (mdbNext (cteMDBNode cte')) = Some cte'; is_derived' (ctes_of sa) (mdbNext (cteMDBNode cte')) cap (cteCap cte'); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode cte'); ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; mdbNext (cteMDBNode cte') \<noteq> dest; src = mdbNext (cteMDBNode cte'); mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte')\<rbrakk> \<Longrightarrow> valid_dlist (ctes_of sa)
 2. \<And>sa x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte') \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa (mdbNext (cteMDBNode cte')) = Some cte'; is_derived' (ctes_of sa) (mdbNext (cteMDBNode cte')) cap (cteCap cte'); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode cte'); ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; mdbNext (cteMDBNode cte') \<noteq> dest; src = mdbNext (cteMDBNode cte'); mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte')\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte') \<noteq> 0
 3. \<And>sa x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte') \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; capAligned cap; valid_objs' sa; ctes_of sa (mdbNext (cteMDBNode cte')) = Some cte'; is_derived' (ctes_of sa) (mdbNext (cteMDBNode cte')) cap (cteCap cte'); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode cte'); ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; mdbNext (cteMDBNode cte') \<noteq> dest; src = mdbNext (cteMDBNode cte'); mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte'); \<exists>cte'a. ctes_of sa (mdbNext (cteMDBNode cte')) = Some cte'a \<and> mdbPrev (cteMDBNode cte'a) = mdbNext (cteMDBNode cte')\<rbrakk> \<Longrightarrow> False
 4. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest
 5. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src; mdbNext (cteMDBNode cte) \<noteq> dest; mdbNext (cteMDBNode cte) = src\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode ctea) = mdbPrev (cteMDBNode cte')
 6. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src; mdbNext (cteMDBNode cte) \<noteq> dest; mdbNext (cteMDBNode cte) \<noteq> src; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> \<exists>cte'a. (\<exists>z. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some z \<and> cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)) z = cte'a) \<and> mdbPrev (cteMDBNode cte'a) = mdbPrev (cteMDBNode cte') proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> valid_dlist (ctes_of sa)
 2. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode ctea) \<noteq> 0
 3. \<And>sa ctea x cte cte'. \<lbrakk>mdbNext (cteMDBNode ctea) \<noteq> 0; mdbPrev (cteMDBNode cte') \<noteq> dest; pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = 0; mdbNext (cteMDBNode x) = 0; valid_dlist (ctes_of sa); ctes_of sa 0 = None; mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); no_loops (ctes_of sa); mdbPrev (cteMDBNode cte') \<noteq> mdbNext (cteMDBNode ctea); mdbPrev (cteMDBNode cte') \<noteq> src; ctes_of sa (mdbPrev (cteMDBNode cte')) = Some cte; ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte'; mdbNext (cteMDBNode ctea) \<noteq> dest; mdbNext (cteMDBNode ctea) \<noteq> src; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode ctea); \<exists>cte'. ctes_of sa (mdbNext (cteMDBNode ctea)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!