theory Finalise_DR

lemma swap_cap_corres:
  "dcorres dc \<top> (valid_idle and valid_mdb and cte_at slot_a and cte_at slot_b
                 and valid_etcbs and K (slot_a \<noteq> slot_b)
                 and not_idle_thread (fst slot_a)
                 and not_idle_thread (fst slot_b))
     (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a)
               (transform_cap cap_b) (transform_cslot_ptr slot_b))
     (cap_swap cap_a slot_a cap_b slot_b)" proof - note inj_on_insert[iff del] show ?thesis supply if_cong[cong] apply (simp add: swap_cap_def cap_swap_def) apply (rule corres_guard_imp) apply (rule corres_split_nor[OF set_cap_corres[OF refl refl]]) apply (rule corres_split_nor[OF set_cap_corres[OF refl refl]]) apply (simp add: swap_parents_def[unfolded Fun.swap_def] set_original_def
                           set_cdt_modify gets_fold_into_modify bind_assoc
                           cap_swap_ext_def update_cdt_list_def set_cdt_list_modify) apply (simp add: gets_fold_into_modify modify_modify o_def) apply (rule_tac P'="K (slot_a \<noteq> slot_b) and cte_at slot_a and cte_at slot_b
                                and (\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s))
                                and no_mloop o cdt"
                     and P=\<top> in corres_modify) apply (clarsimp simp:transform_def transform_current_thread_def
                               transform_asid_table_def transform_objects_def
                               transform_cdt_def split del: if_split) apply (rule sym) apply (subgoal_tac "inj_on transform_cslot_ptr
                     ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s'))
                       \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b") apply (elim conjE) apply (subst map_lift_over_upd, erule subset_inj_on) apply (safe elim!: ranE, simp_all split: if_split_asm,
                   simp_all add: ranI)[1] apply (subst map_lift_over_upd, erule subset_inj_on) apply (safe elim!: ranE, simp_all split: if_split_asm,
                   simp_all add: ranI)[1] apply (subst map_lift_over_if_eq_twice) apply (erule subset_inj_on, fastforce) apply (rule ext) apply (cases slot_a, cases slot_b) apply (simp split del: if_split) apply (intro if_cong[OF refl],
                  simp_all add: map_lift_over_eq_Some inj_on_eq_iff[where f=transform_cslot_ptr]
                                ranI domI)[1] apply (subst subset_inj_on, assumption, fastforce)+ prefer 2 apply (subst subset_inj_on, assumption, fastforce)+ apply (auto simp: map_lift_over_eq_Some inj_on_eq_iff[where f=transform_cslot_ptr]
                              ranI domI
                       intro: map_lift_over_f_eq[THEN iffD2, OF _ refl]
                        elim: subset_inj_on)[2] apply (clarsimp simp: no_cdt_loop_mloop) apply (rule_tac s=s' in transform_cdt_slot_inj_on_cte_at[where P=\<top>]) apply (auto simp: swp_def dest: mdb_cte_atD
                      elim!: ranE)[1] apply (wp set_cap_caps_of_state2 set_cap_idle
                    | simp add: swp_def cte_wp_at_caps_of_state)+ apply clarsimp apply (clarsimp simp: cte_wp_at_caps_of_state valid_mdb_def) apply (safe intro!: mdb_cte_atI) apply (auto simp: swp_def cte_wp_at_caps_of_state not_idle_thread_def
                   dest: mdb_cte_atD elim!: ranE) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and K (slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a) (transform_cap cap_b) (transform_cslot_ptr slot_b)) (cap_swap cap_a slot_a cap_b slot_b) proof (state)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and K (slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a) (transform_cap cap_b) (transform_cslot_ptr slot_b)) (cap_swap cap_a slot_a cap_b slot_b) proof (state)
this:
inj_on ?f (insert ?a ?A) = (inj_on ?f ?A \<and> ?f ?a \<notin> ?f ` (?A - {?a}))

goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and K (slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a) (transform_cap cap_b) (transform_cslot_ptr slot_b)) (cap_swap cap_a slot_a cap_b slot_b) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and K (slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a) (transform_cap cap_b) (transform_cslot_ptr slot_b)) (cap_swap cap_a slot_a cap_b slot_b) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and K (slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a) (transform_cap cap_b) (transform_cslot_ptr slot_b)) (cap_swap cap_a slot_a cap_b slot_b) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) (do y <- KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b);
y <- KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a);
swap_parents (transform_cslot_ptr slot_a) (transform_cslot_ptr slot_b)
od) (do y <- CSpaceAcc_A.set_cap cap_b slot_a;
y <- CSpaceAcc_A.set_cap cap_a slot_b;
slot1_p <- gets (\<lambda>s. cdt s slot_a);
slot2_p <- gets (\<lambda>s. cdt s slot_b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some slot_a then Some slot_b else if cdt n = Some slot_b then Some slot_a else cdt n)(slot_a := if cdt slot_b = Some slot_a then Some slot_b else if cdt slot_b = Some slot_b then Some slot_a else cdt slot_b, slot_b := if cdt slot_a = Some slot_a then Some slot_b else if cdt slot_a = Some slot_b then Some slot_a else cdt slot_a));
y <- cap_swap_ext slot_a slot_b slot1_p slot2_p;
is_original <- gets is_original_cap;
y <- set_original slot_a (is_original slot_b);
set_original slot_b (is_original slot_a)
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do y <- KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b);
y <- KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a);
swap_parents (transform_cslot_ptr slot_a) (transform_cslot_ptr slot_b)
od) (do y <- CSpaceAcc_A.set_cap cap_b slot_a;
y <- CSpaceAcc_A.set_cap cap_a slot_b;
slot1_p <- gets (\<lambda>s. cdt s slot_a);
slot2_p <- gets (\<lambda>s. cdt s slot_b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some slot_a then Some slot_b else if cdt n = Some slot_b then Some slot_a else cdt n)(slot_a := if cdt slot_b = Some slot_a then Some slot_b else if cdt slot_b = Some slot_b then Some slot_a else cdt slot_b, slot_b := if cdt slot_a = Some slot_a then Some slot_b else if cdt slot_a = Some slot_b then Some slot_a else cdt slot_a));
y <- cap_swap_ext slot_a slot_b slot1_p slot2_p;
is_original <- gets is_original_cap;
y <- set_original slot_a (is_original slot_b);
set_original slot_b (is_original slot_a)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a);
swap_parents (transform_cslot_ptr slot_a) (transform_cslot_ptr slot_b)
od) (do y <- CSpaceAcc_A.set_cap cap_a slot_b;
slot1_p <- gets (\<lambda>s. cdt s slot_a);
slot2_p <- gets (\<lambda>s. cdt s slot_b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some slot_a then Some slot_b else if cdt n = Some slot_b then Some slot_a else cdt n)(slot_a := if cdt slot_b = Some slot_a then Some slot_b else if cdt slot_b = Some slot_b then Some slot_a else cdt slot_b, slot_b := if cdt slot_a = Some slot_a then Some slot_b else if cdt slot_a = Some slot_b then Some slot_a else cdt slot_a));
y <- cap_swap_ext slot_a slot_b slot1_p slot2_p;
is_original <- gets is_original_cap;
y <- set_original slot_a (is_original slot_b);
set_original slot_b (is_original slot_a)
od)
 2. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. ?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. ?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. dcorres dc ?R11 ?R'11 (swap_parents (transform_cslot_ptr slot_a) (transform_cslot_ptr slot_b)) (do slot1_p <- gets (\<lambda>s. cdt s slot_a);
slot2_p <- gets (\<lambda>s. cdt s slot_b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some slot_a then Some slot_b else if cdt n = Some slot_b then Some slot_a else cdt n)(slot_a := if cdt slot_b = Some slot_a then Some slot_b else if cdt slot_b = Some slot_b then Some slot_a else cdt slot_b, slot_b := if cdt slot_a = Some slot_a then Some slot_b else if cdt slot_a = Some slot_b then Some slot_a else cdt slot_a));
y <- cap_swap_ext slot_a slot_b slot1_p slot2_p;
is_original <- gets is_original_cap;
y <- set_original slot_a (is_original slot_b);
set_original slot_b (is_original slot_a)
od)
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x. ?R11\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. ?R'11\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. dcorres dc ?R11 ?R'11 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd x)(transform_cslot_ptr slot_a := if cd (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if cd (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd (transform_cslot_ptr slot_a))))) (do slot1_p <- gets (\<lambda>s. cdt s slot_a);
slot2_p <- gets (\<lambda>s. cdt s slot_b);
y <- modify (\<lambda>s. s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>);
x <- modify (\<lambda>s. cdt_list_update (\<lambda>_. (cdt_list s)(slot_a := cdt_list s slot_b, slot_b := cdt_list s slot_a)) s);
y <- modify (\<lambda>s. cdt_list_update (\<lambda>_. case if slot2_p = Some slot_a then Some slot_b else if slot2_p = Some slot_b then Some slot_a else slot2_p of None \<Rightarrow> case if slot1_p = Some slot_a then Some slot_b else if slot1_p = Some slot_b then Some slot_a else slot1_p of None \<Rightarrow> cdt_list s | Some slot2_p \<Rightarrow> (cdt_list s)(slot2_p := list_replace (cdt_list s slot2_p) slot_a slot_b) | Some slot1_pa \<Rightarrow> case if slot1_p = Some slot_a then Some slot_b else if slot1_p = Some slot_b then Some slot_a else slot1_p of None \<Rightarrow> (cdt_list s)(slot1_pa := list_replace (cdt_list s slot1_pa) slot_b slot_a) | Some slot2_p \<Rightarrow> if slot1_pa = slot2_p then (cdt_list s)(slot1_pa := list_swap (cdt_list s slot1_pa) slot_a slot_b) else (cdt_list s)(slot1_pa := list_replace (cdt_list s slot1_pa) slot_b slot_a, slot2_p := list_replace (cdt_list s slot2_p) slot_a slot_b)) s);
is_original <- gets is_original_cap;
y <- modify (\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(slot_a := is_original slot_b)\<rparr>);
modify (\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(slot_b := is_original slot_a)\<rparr>)
od)
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x. ?R11\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. ?R'11\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. dcorres dc ?R11 ?R'11 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd x)(transform_cslot_ptr slot_a := if cd (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if cd (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd (transform_cslot_ptr slot_a))))) (modify (\<lambda>s. s\<lparr>cdt_list := case if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b of None \<Rightarrow> case if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)) slot2_p) slot_a slot_b) | Some slot1_p \<Rightarrow> case if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)) slot1_p) slot_b slot_a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)) slot1_p) slot_a slot_b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)) slot1_p) slot_b slot_a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>))(slot_a := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_b, slot_b := cdt_list (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>) slot_a)) (s\<lparr>cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a)\<rparr>)) slot2_p) slot_a slot_b), cdt := (\<lambda>n. if cdt s n = Some slot_a then Some slot_b else if cdt s n = Some slot_b then Some slot_a else cdt s n)(slot_a := if cdt s slot_b = Some slot_a then Some slot_b else if cdt s slot_b = Some slot_b then Some slot_a else cdt s slot_b, slot_b := if cdt s slot_a = Some slot_a then Some slot_b else if cdt s slot_a = Some slot_b then Some slot_a else cdt s slot_a), is_original_cap := (is_original_cap s)(slot_a := is_original_cap s slot_b, slot_b := is_original_cap s slot_a)\<rparr>))
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x. ?R11\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. ?R'11\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk>True; (K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd x)(transform_cslot_ptr slot_a := if cd (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if cd (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if cd (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else cd (transform_cslot_ptr slot_a))) s, s'\<lparr>cdt_list := case if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b of None \<Rightarrow> case if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)) slot2_p) slot_a slot_b) | Some slot1_p \<Rightarrow> case if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)) slot1_p) slot_b slot_a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)) slot1_p) slot_a slot_b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)) slot1_p) slot_b slot_a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>))(slot_a := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_b, slot_b := cdt_list (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>) slot_a)) (s'\<lparr>cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)\<rparr>)) slot2_p) slot_a slot_b), cdt := (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a), is_original_cap := (is_original_cap s')(slot_a := is_original_cap s' slot_b, slot_b := is_original_cap s' slot_a)\<rparr>) \<in> {ss'. transform (snd ss') = fst ss'}
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr ((\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a)) = (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a))
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = map_lift_over transform_cslot_ptr ((\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = map_lift_over transform_cslot_ptr ((\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 3. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 5. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = map_lift_over transform_cslot_ptr ((\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b, slot_b := if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 3. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 5. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> {slot_b} \<union> set_option (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a) \<union> dom ((\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b)) \<union> ran ((\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b)) \<subseteq> {slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = (map_lift_over transform_cslot_ptr ((\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b)))(transform_cslot_ptr slot_b := map_option transform_cslot_ptr (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 3. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 4. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 6. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = (map_lift_over transform_cslot_ptr ((\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n)(slot_a := if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b)))(transform_cslot_ptr slot_b := map_option transform_cslot_ptr (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 3. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 5. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> {slot_a} \<union> set_option (if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b) \<union> dom (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n) \<union> ran (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n) \<subseteq> {slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = (map_lift_over transform_cslot_ptr (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n))(transform_cslot_ptr slot_a := map_option transform_cslot_ptr (if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b), transform_cslot_ptr slot_b := map_option transform_cslot_ptr (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 3. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 4. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 6. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = (map_lift_over transform_cslot_ptr (\<lambda>n. if cdt s' n = Some slot_a then Some slot_b else if cdt s' n = Some slot_b then Some slot_a else cdt s' n))(transform_cslot_ptr slot_a := map_option transform_cslot_ptr (if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b), transform_cslot_ptr slot_b := map_option transform_cslot_ptr (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 3. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 5. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s') \<union> {slot_a, slot_b} \<union> set_option (Some slot_b) \<union> set_option (Some slot_a))
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then map_option transform_cslot_ptr (Some slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then map_option transform_cslot_ptr (Some slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := map_option transform_cslot_ptr (if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b), transform_cslot_ptr slot_b := map_option transform_cslot_ptr (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 3. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 4. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 6. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a)) = (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then map_option transform_cslot_ptr (Some slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then map_option transform_cslot_ptr (Some slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := map_option transform_cslot_ptr (if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b), transform_cslot_ptr slot_b := map_option transform_cslot_ptr (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 3. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 5. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s' x. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b\<rbrakk> \<Longrightarrow> ((\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a))) x = ((\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then map_option transform_cslot_ptr (Some slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then map_option transform_cslot_ptr (Some slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := map_option transform_cslot_ptr (if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b), transform_cslot_ptr slot_b := map_option transform_cslot_ptr (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))) x
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 3. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 5. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s' x a b aa ba. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' slot_a \<noteq> Some slot_a; cdt s' slot_b \<noteq> Some slot_b; slot_a = (a, b); slot_b = (aa, ba)\<rbrakk> \<Longrightarrow> ((\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_b), transform_cslot_ptr slot_b := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_a) then Some (transform_cslot_ptr slot_b) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot_b) then Some (transform_cslot_ptr slot_a) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr slot_a))) x = ((\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_a) then map_option transform_cslot_ptr (Some slot_b) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr slot_b) then map_option transform_cslot_ptr (Some slot_a) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr slot_a := map_option transform_cslot_ptr (if cdt s' slot_b = Some slot_a then Some slot_b else if cdt s' slot_b = Some slot_b then Some slot_a else cdt s' slot_b), transform_cslot_ptr slot_b := map_option transform_cslot_ptr (if cdt s' slot_a = Some slot_a then Some slot_b else if cdt s' slot_a = Some slot_b then Some slot_a else cdt s' slot_a))) x
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 3. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 5. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba)\<rbrakk> \<Longrightarrow> (if x = transform_cslot_ptr (aa, ba) then if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = Some (transform_cslot_ptr (a, b)) then Some (transform_cslot_ptr (aa, ba)) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = Some (transform_cslot_ptr (aa, ba)) then Some (transform_cslot_ptr (a, b)) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) else if x = transform_cslot_ptr (a, b) then if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) then Some (transform_cslot_ptr (aa, ba)) else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) then Some (transform_cslot_ptr (a, b)) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr (a, b)) then Some (transform_cslot_ptr (aa, ba)) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr (aa, ba)) then Some (transform_cslot_ptr (a, b)) else map_lift_over transform_cslot_ptr (cdt s') x) = (if x = transform_cslot_ptr (aa, ba) then map_option transform_cslot_ptr (if cdt s' (a, b) = Some (aa, ba) then Some (a, b) else cdt s' (a, b)) else if x = transform_cslot_ptr (a, b) then map_option transform_cslot_ptr (if cdt s' (aa, ba) = Some (a, b) then Some (aa, ba) else cdt s' (aa, ba)) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr (a, b)) then Some (transform_cslot_ptr (aa, ba)) else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr (aa, ba)) then Some (transform_cslot_ptr (a, b)) else map_lift_over transform_cslot_ptr (cdt s') x)
 2. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 3. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 5. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba); x = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> (cdt s' (a, b) = Some (aa, ba) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (ab, bb) = Some (a, b))) \<longrightarrow> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> aa = a \<and> ba = b) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (a, b)))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> aa = a \<and> ba = b) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (aa, ba) = Some (ab, bb)))))) \<and> (cdt s' (a, b) \<noteq> Some (aa, ba) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (ab, bb) = Some (a, b))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (a, b)))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))))
 2. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba); x = transform_cslot_ptr (a, b)\<rbrakk> \<Longrightarrow> (cdt s' (aa, ba) = Some (a, b) \<longrightarrow> ((\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))) \<longrightarrow> (inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> a = aa \<and> b = ba) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (a, b) \<noteq> Some (aa, ba)))) \<longrightarrow> (inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))))) \<and> (cdt s' (aa, ba) \<noteq> Some (a, b) \<longrightarrow> ((\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (ab, bb) = Some (aa, ba))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (a, b) \<noteq> Some (aa, ba)))) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (ab, bb) = Some (aa, ba))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)))))
 3. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 4. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 6. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba); x = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> (cdt s' (a, b) = Some (aa, ba) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> True \<and> cdt s' (ab, bb) = Some (a, b))) \<longrightarrow> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> aa = a \<and> ba = b) \<and> ((True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (a, b)))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> aa = a \<and> ba = b) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb)))))) \<and> (cdt s' (a, b) \<noteq> Some (aa, ba) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> True \<and> cdt s' (ab, bb) = Some (a, b))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b))) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> ((True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (a, b)))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b))) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))))
 2. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba); x = transform_cslot_ptr (a, b)\<rbrakk> \<Longrightarrow> (cdt s' (aa, ba) = Some (a, b) \<longrightarrow> ((\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))) \<longrightarrow> (inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> a = aa \<and> b = ba) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (a, b) \<noteq> Some (aa, ba)))) \<longrightarrow> (inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))))) \<and> (cdt s' (aa, ba) \<noteq> Some (a, b) \<longrightarrow> ((\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (ab, bb) = Some (aa, ba))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (a, b) \<noteq> Some (aa, ba)))) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (ab, bb) = Some (aa, ba))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)))))
 3. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 4. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 6. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba); x = transform_cslot_ptr (a, b)\<rbrakk> \<Longrightarrow> (cdt s' (aa, ba) = Some (a, b) \<longrightarrow> ((\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))) \<longrightarrow> (inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> a = aa \<and> b = ba) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (a, b) \<noteq> Some (aa, ba)))) \<longrightarrow> (inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))))) \<and> (cdt s' (aa, ba) \<noteq> Some (a, b) \<longrightarrow> ((\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (a, b) = Some (ab, bb))) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (ab, bb) = Some (aa, ba))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (a, b) \<noteq> Some (aa, ba)))) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' (ab, bb) = Some (aa, ba))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> ((inj_on transform_cslot_ptr (dom (cdt s') \<union> ran (cdt s')) \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)))))
 2. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba); x = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> (cdt s' (a, b) = Some (aa, ba) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> True \<and> cdt s' (ab, bb) = Some (a, b))) \<longrightarrow> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> aa = a \<and> ba = b) \<and> ((True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (a, b)))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> aa = a \<and> ba = b) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb)))))) \<and> (cdt s' (a, b) \<noteq> Some (aa, ba) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> True \<and> cdt s' (ab, bb) = Some (a, b))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b))) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> ((True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (a, b)))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b))) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))))
 3. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 4. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 6. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba); x = transform_cslot_ptr (a, b)\<rbrakk> \<Longrightarrow> (cdt s' (aa, ba) = Some (a, b) \<longrightarrow> ((\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (a, b) = Some (ab, bb))) \<longrightarrow> (True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> a = aa \<and> b = ba) \<and> ((True \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (a, b) \<noteq> Some (aa, ba)))) \<longrightarrow> (True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (a, b) = Some (ab, bb))))) \<and> (cdt s' (aa, ba) \<noteq> Some (a, b) \<longrightarrow> ((\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> (\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (a, b) = Some (ab, bb))) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> True \<and> cdt s' (ab, bb) = Some (aa, ba))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> ((True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)))) \<and> ((True \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (a, b) \<noteq> Some (aa, ba)))) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<and> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> True \<and> cdt s' (ab, bb) = Some (aa, ba))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> ((True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (aa, ba)))) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)))))
 2. \<And>s' x a b aa ba. \<lbrakk>a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>_. True) (a, b) s'; cte_wp_at (\<lambda>_. True) (aa, ba) s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); inj_on transform_cslot_ptr (insert (a, b) (insert (aa, ba) (dom (cdt s') \<union> ran (cdt s')))); cdt s' (a, b) \<noteq> Some (a, b); cdt s' (aa, ba) \<noteq> Some (aa, ba); slot_a = (a, b); slot_b = (aa, ba); x = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> (cdt s' (a, b) = Some (aa, ba) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> True \<and> cdt s' (ab, bb) = Some (a, b))) \<longrightarrow> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> aa = a \<and> ba = b) \<and> ((True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (a, b)))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> aa = a \<and> ba = b) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> (\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb)))))) \<and> (cdt s' (a, b) \<noteq> Some (aa, ba) \<longrightarrow> ((\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> True \<and> cdt s' (ab, bb) = Some (a, b))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b))) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> ((True \<longrightarrow> (\<forall>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (ab, bb) \<noteq> Some (a, b)))) \<longrightarrow> ((\<exists>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> True \<and> cdt s' (aa, ba) = Some (ab, bb))) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b))) \<and> ((True \<longrightarrow> (\<forall>aa ba. transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s' (aa, ba) \<noteq> Some (a, b)))) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))))
 3. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 4. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 6. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr (insert slot_a (insert slot_b (dom (cdt s') \<union> ran (cdt s'))))
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>s' x. \<lbrakk>slot_a \<noteq> slot_b; cte_wp_at (\<lambda>_. True) slot_a s'; cte_wp_at (\<lambda>_. True) slot_b s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); no_mloop (cdt s'); x \<in> insert slot_a (insert slot_b (dom (cdt s') \<union> ran (cdt s')))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s'
 2. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 4. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q11\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_b) (transform_cap cap_a) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrace>?Q'11\<rbrace> CSpaceAcc_A.set_cap cap_a slot_b \<lbrace>\<lambda>x. K (slot_a \<noteq> slot_b) and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and no_mloop \<circ> cdt\<rbrace>
 3. \<lbrace>?Q4\<rbrace> KHeap_D.set_cap (transform_cslot_ptr slot_a) (transform_cap cap_b) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q11\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap_b slot_a \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst slot_b \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'11\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and (\<lambda>y. slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) s \<Longrightarrow> ((\<lambda>s. valid_idle s \<and> fst slot_a \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_idle s \<and> valid_mdb s \<and> (\<exists>cap. caps_of_state s slot_a = Some cap) \<and> (\<exists>cap. caps_of_state s slot_b = Some cap) \<and> valid_etcbs s \<and> slot_a \<noteq> slot_b \<and> not_idle_thread (fst slot_a) s \<and> not_idle_thread (fst slot_b) s \<Longrightarrow> fst slot_a \<noteq> idle_thread s \<and> fst slot_b \<noteq> idle_thread s \<and> mdb_cte_at (\<lambda>y. y \<noteq> slot_a \<longrightarrow> y \<noteq> slot_b \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s) \<and> no_mloop (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_idle s; valid_mdb s; caps_of_state s slot_a = Some cap; caps_of_state s slot_b = Some capa; valid_etcbs s; slot_a \<noteq> slot_b; not_idle_thread (fst slot_a) s; not_idle_thread (fst slot_b) s\<rbrakk> \<Longrightarrow> fst slot_a \<noteq> idle_thread s \<and> fst slot_b \<noteq> idle_thread s \<and> mdb_cte_at (\<lambda>y. y \<noteq> slot_a \<longrightarrow> y \<noteq> slot_b \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s) \<and> no_mloop (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>valid_idle s; caps_of_state s slot_a = Some cap; caps_of_state s slot_b = Some capa; valid_etcbs s; slot_a \<noteq> slot_b; not_idle_thread (fst slot_a) s; not_idle_thread (fst slot_b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> fst slot_a \<noteq> idle_thread s \<and> fst slot_b \<noteq> idle_thread s \<and> mdb_cte_at (\<lambda>y. y \<noteq> slot_a \<longrightarrow> y \<noteq> slot_b \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>s cap capa. \<lbrakk>valid_idle s; caps_of_state s slot_a = Some cap; caps_of_state s slot_b = Some capa; valid_etcbs s; slot_a \<noteq> slot_b; not_idle_thread (fst slot_a) s; not_idle_thread (fst slot_b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); fst slot_a = idle_thread s\<rbrakk> \<Longrightarrow> False
 2. \<And>s cap capa. \<lbrakk>valid_idle s; caps_of_state s slot_a = Some cap; caps_of_state s slot_b = Some capa; valid_etcbs s; slot_a \<noteq> slot_b; not_idle_thread (fst slot_a) s; not_idle_thread (fst slot_b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); fst slot_b = idle_thread s\<rbrakk> \<Longrightarrow> False
 3. \<And>s cap capa a b aa ba. \<lbrakk>valid_idle s; caps_of_state s slot_a = Some cap; caps_of_state s slot_b = Some capa; valid_etcbs s; slot_a \<noteq> slot_b; not_idle_thread (fst slot_a) s; not_idle_thread (fst slot_b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); cdt s (a, b) = Some (aa, ba); (aa, ba) \<noteq> slot_a; (aa, ba) \<noteq> slot_b\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (aa, ba) = Some cap
 4. \<And>s cap capa a b aa ba. \<lbrakk>valid_idle s; caps_of_state s slot_a = Some cap; caps_of_state s slot_b = Some capa; valid_etcbs s; slot_a \<noteq> slot_b; not_idle_thread (fst slot_a) s; not_idle_thread (fst slot_b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); cdt s (a, b) = Some (aa, ba); (a, b) \<noteq> slot_a; (a, b) \<noteq> slot_b\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (a, b) = Some cap proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>s cap capa a b aa ba. ?x1504 s cap capa a b aa ba (aa, ba) \<equiv>\<^sup>? \<lambda>s cap capa a b aa ba. ?x1503 s cap capa a b aa ba (aa, ba)
\<lambda>s cap capa a b aa ba. ?x1482 s cap capa a b aa ba (aa, ba) \<equiv>\<^sup>? \<lambda>s cap capa a b aa ba. ?x1481 s cap capa a b aa ba (aa, ba) proof (state)
this:
dcorres dc (\<lambda>_. True) (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) slot_a and cte_wp_at (\<lambda>_. True) slot_b and valid_etcbs and K (slot_a \<noteq> slot_b) and not_idle_thread (fst slot_a) and not_idle_thread (fst slot_b)) (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a) (transform_cap cap_b) (transform_cslot_ptr slot_b)) (cap_swap cap_a slot_a cap_b slot_b)

goal:
No subgoals!