theory CNodeInv_R

lemma cteSwap_valid_pspace'[wp]:
  "\<lbrace>valid_pspace' and
    cte_wp_at' (weak_derived' c o cteCap) c1 and
    cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> (cteCap cc) = c) c1 and
    cte_wp_at' (weak_derived' c' o cteCap) c2 and
    cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> (cteCap cc) = c') c2 and
    valid_cap' c and valid_cap' c' and
    K (c1 \<noteq> c2)\<rbrace>
  cteSwap c c1 c' c2
  \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" unfolding cteSwap_def apply (simp add: pred_conj_def valid_pspace'_def valid_mdb'_def) apply (rule hoare_pre) apply wp apply (wp getCTE_inv getCTE_wp) apply (strengthen imp_consequent, strengthen ctes_of_strng) apply ((wp sch_act_wf_lift valid_queues_lift
                    cur_tcb_lift updateCap_no_0  updateCap_ctes_of_wp
                    hoare_vcg_ex_lift updateMDB_cte_wp_at_other getCTE_wp
                  | rule hoare_drop_imps)+)[6] apply (clarsimp simp: valid_pspace_no_0[unfolded valid_pspace'_def valid_mdb'_def]
                        cte_wp_at_ctes_of) apply (subgoal_tac "c2 \<in> dom (modify_map
               (modify_map
                 (modify_map
                   (modify_map (ctes_of s) c1 (cteCap_update (%_. c'))) c2
                   (cteCap_update (%_. c)))
                 (mdbPrev (cteMDBNode cte))
                 (cteMDBNode_update (mdbNext_update (%_. c2))))
               (mdbNext (cteMDBNode cte))
               (cteMDBNode_update (mdbPrev_update (%_. c2))))") apply (erule domE) apply (intro exI) apply (rule conjI) apply (clarsimp simp: modify_map_def cte_wp_at_ctes_of) apply (rule refl) apply (case_tac cte) apply (case_tac cteb) apply (rule_tac dest_node = "cteMDBNode cteb" in
     mdb_swap.cteSwap_valid_mdb_helper [simplified const_def]) apply (rule mdb_swap.intro) apply (rule mdb_ptr.intro) apply (erule vmdb.intro) apply (rule mdb_ptr_axioms.intro) apply simp apply (rule mdb_ptr.intro) apply (erule vmdb.intro) apply (rule mdb_ptr_axioms.intro) apply (simp add: cte_wp_at_ctes_of) apply (erule mdb_swap_axioms.intro) apply clarsimp apply (erule weak_derived_sym') apply clarsimp apply (erule weak_derived_sym') apply (simp) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 and valid_cap' c and valid_cap' c' and K (c1 \<noteq> c2)\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 and valid_cap' c and valid_cap' c' and K (c1 \<noteq> c2)\<rbrace> do cte1 <- getCTE c1;
updateCap c1 c';
updateCap c2 c;
mdb1 <- return (cteMDBNode cte1);
updateMDB (mdbPrev mdb1) (mdbNext_update (\<lambda>_. c2));
updateMDB (mdbNext mdb1) (mdbPrev_update (\<lambda>_. c2));
cte2 <- getCTE c2;
mdb2 <- return (cteMDBNode cte2);
updateMDB c1 (const mdb2);
updateMDB c2 (const mdb1);
updateMDB (mdbPrev mdb2) (mdbNext_update (\<lambda>_. c1));
updateMDB (mdbNext mdb2) (mdbPrev_update (\<lambda>_. c1))
od \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. valid_objs' x \<and> pspace_aligned' x \<and> pspace_distinct' x \<and> no_0_obj' x \<and> valid_mdb_ctes (ctes_of x) \<and> cte_wp_at' (weak_derived' c \<circ> cteCap) c1 x \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 x \<and> cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 x \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 x \<and> valid_cap' c x \<and> valid_cap' c' x \<and> c1 \<noteq> c2\<rbrace> do cte1 <- getCTE c1;
y <- updateCap c1 c';
y <- updateCap c2 c;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2));
cte2 <- getCTE c2;
y <- updateMDB c1 (const (cteMDBNode cte2));
y <- updateMDB c2 (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. c1));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. c1))
od \<lbrace>\<lambda>rv x. valid_objs' x \<and> pspace_aligned' x \<and> pspace_distinct' x \<and> no_0_obj' x \<and> valid_mdb_ctes (ctes_of x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cte1 <- getCTE c1;
y <- updateCap c1 c';
y <- updateCap c2 c;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2));
cte2 <- getCTE c2;
y <- updateMDB c1 (const (cteMDBNode cte2));
y <- updateMDB c2 (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. c1));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. c1))
od \<lbrace>\<lambda>rv x. valid_objs' x \<and> pspace_aligned' x \<and> pspace_distinct' x \<and> no_0_obj' x \<and> valid_mdb_ctes (ctes_of x)\<rbrace>
 2. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s \<and> cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s \<and> valid_cap' c s \<and> valid_cap' c' s \<and> c1 \<noteq> c2 \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>cte1 y ya yb yc. \<lbrace>?P'79 cte1 y ya yb yc\<rbrace> getCTE c2 \<lbrace>\<lambda>rv s. valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteMDBNode_update (const (cteMDBNode rv)))) c2 (cteMDBNode_update (const (cteMDBNode cte1)))) (mdbPrev (cteMDBNode rv)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode rv)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))\<rbrace>
 2. \<And>cte1 y ya yb. \<lbrace>?B7 cte1 y ya yb\<rbrace> updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2)) \<lbrace>\<lambda>yc s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> ?P'79 cte1 y ya yb yc s\<rbrace>
 3. \<And>cte1 y ya. \<lbrace>?B6 cte1 y ya\<rbrace> updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2)) \<lbrace>?B7 cte1 y ya\<rbrace>
 4. \<And>cte1 y. \<lbrace>?B5 cte1 y\<rbrace> updateCap c2 c \<lbrace>?B6 cte1 y\<rbrace>
 5. \<And>cte1. \<lbrace>?B4 cte1\<rbrace> updateCap c1 c' \<lbrace>?B5 cte1\<rbrace>
 6. \<lbrace>?Q\<rbrace> getCTE c1 \<lbrace>?B4\<rbrace>
 7. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s \<and> cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s \<and> valid_cap' c s \<and> valid_cap' c' s \<and> c1 \<noteq> c2 \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cte1 y ya yb. \<lbrace>?B7 cte1 y ya yb\<rbrace> updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2)) \<lbrace>\<lambda>yc s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> (cte_wp_at' (\<lambda>_. True) c2 s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) c2 s \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteMDBNode_update (const (cteMDBNode cte)))) c2 (cteMDBNode_update (const (cteMDBNode cte1)))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))))\<rbrace>
 2. \<And>cte1 y ya. \<lbrace>?B6 cte1 y ya\<rbrace> updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2)) \<lbrace>?B7 cte1 y ya\<rbrace>
 3. \<And>cte1 y. \<lbrace>?B5 cte1 y\<rbrace> updateCap c2 c \<lbrace>?B6 cte1 y\<rbrace>
 4. \<And>cte1. \<lbrace>?B4 cte1\<rbrace> updateCap c1 c' \<lbrace>?B5 cte1\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE c1 \<lbrace>?B4\<rbrace>
 6. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s \<and> cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s \<and> valid_cap' c s \<and> valid_cap' c' s \<and> c1 \<noteq> c2 \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cte1 y ya yb. \<lbrace>?B7 cte1 y ya yb\<rbrace> updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2)) \<lbrace>\<lambda>r s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> (\<exists>cte. ctes_of s c2 = Some cte \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteMDBNode_update (const (cteMDBNode cte)))) c2 (cteMDBNode_update (const (cteMDBNode cte1)))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1)))))\<rbrace>
 2. \<And>cte1 y ya. \<lbrace>?B6 cte1 y ya\<rbrace> updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2)) \<lbrace>?B7 cte1 y ya\<rbrace>
 3. \<And>cte1 y. \<lbrace>?B5 cte1 y\<rbrace> updateCap c2 c \<lbrace>?B6 cte1 y\<rbrace>
 4. \<And>cte1. \<lbrace>?B4 cte1\<rbrace> updateCap c1 c' \<lbrace>?B5 cte1\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE c1 \<lbrace>?B4\<rbrace>
 6. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s \<and> cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s \<and> valid_cap' c s \<and> valid_cap' c' s \<and> c1 \<noteq> c2 \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s \<and> cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s \<and> valid_cap' c s \<and> valid_cap' c' s \<and> c1 \<noteq> c2 \<Longrightarrow> cte_wp_at' (\<lambda>_. True) c1 s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) c1 s \<and> (valid_objs' and valid_cap' c') s \<and> valid_cap' c s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> no_0 (ctes_of s) \<and> (\<exists>x. no_0 (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) \<and> no_0 (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) \<and> modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some x \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (const (cteMDBNode x)))) c2 (cteMDBNode_update (const (cteMDBNode cte)))) (mdbPrev (cteMDBNode x)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode x)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> \<exists>x. modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some x \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode x))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode x)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode x)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))))\<rbrakk> \<Longrightarrow> \<exists>x. modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some x \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode x))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode x)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode x)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))
 2. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb r. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r\<rbrakk> \<Longrightarrow> \<exists>x. modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some x \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode x))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode x)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode x)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))
 2. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb r. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some (?x252 s cte cteb r) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode (?x252 s cte cteb r)))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode (?x252 s cte cteb r))) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode (?x252 s cte cteb r))) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))
 2. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb r. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some (?x252 s cte cteb r)
 2. \<And>s cte cteb r. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode (?x252 s cte cteb r)))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode (?x252 s cte cteb r))) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode (?x252 s cte cteb r))) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))
 3. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb r. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; (if c2 = mdbNext (cteMDBNode cte) then map_option (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbNext (cteMDBNode cte)))) (if mdbNext (cteMDBNode cte) = mdbPrev (cteMDBNode cte) then Some (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbPrev (cteMDBNode cte))) (cteCap_update (\<lambda>_. c) cteb)) else Some (cteCap_update (\<lambda>_. c) cteb)) else if c2 = mdbPrev (cteMDBNode cte) then Some (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbPrev (cteMDBNode cte))) (cteCap_update (\<lambda>_. c) cteb)) else Some (cteCap_update (\<lambda>_. c) cteb)) = Some r\<rbrakk> \<Longrightarrow> r = ?x252 s cte cteb r
 2. \<And>s cte cteb r. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode (?x252 s cte cteb r)))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode (?x252 s cte cteb r))) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode (?x252 s cte cteb r))) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))
 3. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb r. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode r))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode r)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode r)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))
 2. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb r x1 x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode r))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode r)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode r)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))
 2. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) c1 (cteMDBNode_update (\<lambda>a. cteMDBNode r))) c2 (cteMDBNode_update (\<lambda>a. cteMDBNode cte))) (mdbPrev (cteMDBNode r)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c1)))) (mdbNext (cteMDBNode r)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c1))))
 2. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap (ctes_of s) c1 (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb) c c' r
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?src_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c = ?src_cap271 s cte cteb r x1 x2 x1a x2a
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 4. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (6 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) c1 (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte)
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb)
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) c c' r
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?src_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c = ?src_cap271 s cte cteb r x1 x2 x1a x2a
 5. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 6. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (7 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> vmdb (ctes_of s)
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr_axioms (ctes_of s) c1 (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte)
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb)
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) c c' r
 5. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?src_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c = ?src_cap271 s cte cteb r x1 x2 x1a x2a
 6. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 7. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (6 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr_axioms (ctes_of s) c1 (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte)
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb)
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) c c' r
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?src_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c = ?src_cap271 s cte cteb r x1 x2 x1a x2a
 5. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 6. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (6 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> ctes_of s c1 = Some (CTE (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte))
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb)
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 (?src_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) c c' r
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?src_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c = ?src_cap271 s cte cteb r x1 x2 x1a x2a
 5. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 6. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (5 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr (ctes_of s) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb)
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 x1 (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) c c' r
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 5. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (6 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> vmdb (ctes_of s)
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr_axioms (ctes_of s) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb)
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 x1 (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) c c' r
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 5. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 6. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (5 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_ptr_axioms (ctes_of s) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb)
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 x1 (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) c c' r
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 5. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (5 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> ctes_of s c2 = Some (CTE (?dest_cap271 s cte cteb r x1 x2 x1a x2a) (cteMDBNode cteb))
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 x1 (cteMDBNode cte) c2 (?dest_cap271 s cte cteb r x1 x2 x1a x2a) c c' r
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap (?dest_cap271 s cte cteb r x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> c' = ?dest_cap271 s cte cteb r x1 x2 x1a x2a
 5. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> mdb_swap_axioms (ctes_of s) c1 x1 (cteMDBNode cte) c2 x1a c c' r
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1a\<rbrakk> \<Longrightarrow> c' = x1a
 4. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (6 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> weak_derived' x1 c
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> weak_derived' x1a c'
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 5. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1a\<rbrakk> \<Longrightarrow> c' = x1a
 6. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (6 subgoals):
 1. \<And>s r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c x1; isUntypedCap x1 \<longrightarrow> x1 = c; weak_derived' c' x1a; valid_cap' c s; ctes_of s c2 = Some (CTE x1a x2a); isUntypedCap x1a \<longrightarrow> x1a = c'; valid_cap' c' s; ctes_of s c1 = Some (CTE x1 x2); modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev x2) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext x2) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r\<rbrakk> \<Longrightarrow> weak_derived' x1 c
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> weak_derived' x1a c'
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 5. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1a\<rbrakk> \<Longrightarrow> c' = x1a
 6. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (5 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> weak_derived' x1a c'
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1a\<rbrakk> \<Longrightarrow> c' = x1a
 5. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (5 subgoals):
 1. \<And>s r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c x1; isUntypedCap x1 \<longrightarrow> x1 = c; weak_derived' c' x1a; valid_cap' c s; ctes_of s c2 = Some (CTE x1a x2a); isUntypedCap x1a \<longrightarrow> x1a = c'; valid_cap' c' s; ctes_of s c1 = Some (CTE x1 x2); modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev x2) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext x2) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r\<rbrakk> \<Longrightarrow> weak_derived' x1a c'
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 4. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1a\<rbrakk> \<Longrightarrow> c' = x1a
 5. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 3. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1a\<rbrakk> \<Longrightarrow> c' = x1a
 4. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1\<rbrakk> \<Longrightarrow> c = x1
 2. \<And>s cte cteb r x1 x2 x1a x2a. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte; modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2))) c2 = Some r; cte = CTE x1 x2; cteb = CTE x1a x2a; isUntypedCap x1a\<rbrakk> \<Longrightarrow> c' = x1a
 3. \<And>s cte cteb. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); weak_derived' c (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap cteb); valid_cap' c s; ctes_of s c2 = Some cteb; isUntypedCap (cteCap cteb) \<longrightarrow> cteCap cteb = c'; valid_cap' c' s; c1 \<noteq> c2; ctes_of s c1 = Some cte\<rbrakk> \<Longrightarrow> c2 \<in> dom (modify_map (modify_map (modify_map (modify_map (ctes_of s) c1 (cteCap_update (\<lambda>_. c'))) c2 (cteCap_update (\<lambda>_. c))) (mdbPrev (cteMDBNode cte)) (cteMDBNode_update (mdbNext_update (\<lambda>_. c2)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. c2)))) proof (prove)
goal:
No subgoals!