theory CNode_DR

lemma move_cap_corres:
  "dcorres dc \<top> (cte_wp_at ((=) cap.NullCap) p'
                     and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p
                     and not_idle_thread (fst p')
                     and not_idle_thread (fst p))
     (move_cap (transform_cap cap) (transform_cslot_ptr p)
          (transform_cslot_ptr p'))
     (cap_move cap p p')" proof - note inj_on_insert[iff del] have insert_sub_walk:
    "\<And>p p' S. p \<noteq> p' \<Longrightarrow> insert p S - {p'} = insert p (S - {p'})" by auto show ?thesis supply if_cong[cong] apply (simp add: cap_move_def move_cap_def cap_move_swap_ext_def swap_parents_def
                del: fun_upd_apply) apply (rule stronger_corres_guard_imp) apply (rule corres_split_nor) apply (simp add: insert_cap_orphan_def) apply (rule corres_dummy_return_pr[where b="()"]) apply (rule corres_split[where r'=dc]) apply (rule corres_gets_the) apply simp apply (rule corres_trivial, rule gets_symb_exec_l) apply (rule corres_assert_lhs) apply simp apply (rule set_cap_corres, simp+)[1] apply (wp set_cap_caps_of_state2 set_cap_idle)+ apply (rule corres_split_nor) apply (rule set_cap_corres) apply (simp add: transform_cap_def) apply simp apply (rule dcorres_gets_all_param) apply (rule dcorres_gets_all_param) apply (simp add: swap_parents_def
                           set_original_def set_cdt_modify
                           gets_fold_into_modify modify_modify
                           cap_move_ext_def bind_assoc update_cdt_list_def set_cdt_list_modify) apply (rule conjI, clarsimp) apply (rule_tac P'="cte_at p and cte_at p' and (\<lambda>s. cdt s p' = None)
                         and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop o cdt
                         and (\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s)) and K (p \<noteq> p')" and P=\<top>
                       in corres_inst) apply (rule corres_modify) apply (clarsimp simp: transform_def transform_current_thread_def
                                 transform_cdt_def transform_asid_table_def
                                 transform_objects_def) apply clarsimp apply (rule corres_modify) apply (clarsimp simp: transform_def transform_current_thread_def
                                transform_cdt_def transform_asid_table_def
                                transform_objects_def) apply (subgoal_tac "inj_on transform_cslot_ptr
              ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p") apply (elim conjE) apply (subst map_lift_over_if_eq) apply (erule subset_inj_on, auto elim!: ranE split: if_split_asm)[1] apply (rule sym) apply (simp add: Fun.swap_def split del: if_split) apply (subst map_lift_over_upd[unfolded fun_upd_def],
                    ((erule subset_inj_on, auto elim!: ranE split: if_split_asm)[1]))+ apply (rule ext) apply (cases p, cases p') apply (simp split del: if_split) apply simp apply (subst subset_inj_on map_lift_over_f_eq[OF subset_inj_on],
                  assumption, fastforce)+ apply (simp add: inj_on_eq_iff[where f="transform_cslot_ptr"]
                            ranI domI map_option_eq_Some[THEN trans [OF eq_commute]]) apply (auto simp: inj_on_eq_iff[where f="transform_cslot_ptr"]
                             ranI domI,
                  auto simp: inj_on_eq_iff[where f="transform_cslot_ptr"]
                             ranI domI map_lift_over_eq_Some)[1] 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
                    | simp add: swp_def cte_wp_at_caps_of_state)+ apply clarsimp apply (clarsimp simp: cte_wp_at_caps_of_state
                           caps_of_state_transform_opt_cap
                           transform_cap_def not_idle_thread_def) apply (clarsimp simp: mdb_Null_None[OF _ invs_mdb]) apply (frule invs_mdb) 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) (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) (move_cap (transform_cap cap) (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_move cap p p') proof (state)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) (move_cap (transform_cap cap) (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_move cap p p') 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) (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) (move_cap (transform_cap cap) (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_move cap p p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' S. p \<noteq> p' \<Longrightarrow> insert p S - {p'} = insert p (S - {p'}) proof (state)
this:
?p \<noteq> ?p' \<Longrightarrow> insert ?p ?S - {?p'} = insert ?p (?S - {?p'})

goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) (move_cap (transform_cap cap) (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_move cap p p') proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) (move_cap (transform_cap cap) (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_move cap p p') proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) (move_cap (transform_cap cap) (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_move cap p p') proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) (do y <- insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p');
y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap p';
y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do y <- insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p');
y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap p';
y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (6 subgoals):
 1. dcorres dc ?P4 ?P'4 (insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p')) (CSpaceAcc_A.set_cap cap p')
 2. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 3. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s' proof (prove)
goal (6 subgoals):
 1. dcorres dc ?P4 ?P'4 (do old_cap <- KHeap_D.get_cap (transform_cslot_ptr p');
y <- assert (old_cap = cdl_cap.NullCap);
KHeap_D.set_cap (transform_cslot_ptr p') (transform_cap cap)
od) (CSpaceAcc_A.set_cap cap p')
 2. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 3. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s' proof (prove)
goal (6 subgoals):
 1. dcorres dc ?P4 ?P'4 (do old_cap <- KHeap_D.get_cap (transform_cslot_ptr p');
y <- assert (old_cap = cdl_cap.NullCap);
KHeap_D.set_cap (transform_cslot_ptr p') (transform_cap cap)
od) (do return ();
CSpaceAcc_A.set_cap cap p'
od)
 2. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 3. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s' proof (prove)
goal (9 subgoals):
 1. dcorres dc ?P11 ?P'11 (KHeap_D.get_cap (transform_cslot_ptr p')) (return ())
 2. \<And>old_cap rv'. dc old_cap rv' \<Longrightarrow> dcorres dc (?R11 old_cap) (?R'11 rv') (do y <- assert (old_cap = cdl_cap.NullCap);
KHeap_D.set_cap (transform_cslot_ptr p') (transform_cap cap)
od) (K_bind (CSpaceAcc_A.set_cap cap p') rv')
 3. \<lbrace>?Q11\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>?R11\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> return () \<lbrace>?R'11\<rbrace>
 5. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 6. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P11 and ?Q11 and ?Q4) s
 9. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P'11 and ?Q'11 and ?Q'4) s' proof (prove)
goal (9 subgoals):
 1. dcorres (dc \<circ> the) ?P16 ?P'11 (gets (opt_cap (transform_cslot_ptr p'))) (return ())
 2. \<And>old_cap rv'. dc old_cap rv' \<Longrightarrow> dcorres dc (?R11 old_cap) (?R'11 rv') (do y <- assert (old_cap = cdl_cap.NullCap);
KHeap_D.set_cap (transform_cslot_ptr p') (transform_cap cap)
od) (K_bind (CSpaceAcc_A.set_cap cap p') rv')
 3. \<lbrace>?Q11\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>?R11\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> return () \<lbrace>?R'11\<rbrace>
 5. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 6. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P16 and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and ?Q11 and ?Q4) s
 9. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P'11 and ?Q'11 and ?Q'4) s' proof (prove)
goal (9 subgoals):
 1. dcorres dc ?P16 ?P'11 (gets (opt_cap (transform_cslot_ptr p'))) (return ())
 2. \<And>old_cap rv'. dc old_cap rv' \<Longrightarrow> dcorres dc (?R11 old_cap) (?R'11 rv') (do y <- assert (old_cap = cdl_cap.NullCap);
KHeap_D.set_cap (transform_cslot_ptr p') (transform_cap cap)
od) (K_bind (CSpaceAcc_A.set_cap cap p') rv')
 3. \<lbrace>?Q11\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>?R11\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> return () \<lbrace>?R'11\<rbrace>
 5. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 6. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P16 and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and ?Q11 and ?Q4) s
 9. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P'11 and ?Q'11 and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>old_cap rv'. dc old_cap rv' \<Longrightarrow> dcorres dc (?R11 old_cap) (?R'11 rv') (do y <- assert (old_cap = cdl_cap.NullCap);
KHeap_D.set_cap (transform_cslot_ptr p') (transform_cap cap)
od) (K_bind (CSpaceAcc_A.set_cap cap p') rv')
 2. \<lbrace>?Q11\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>?R11\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> return () \<lbrace>?R'11\<rbrace>
 4. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and ?Q11 and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'11 and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>old_cap rv'. \<lbrakk>dc old_cap rv'; old_cap = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?P23 old_cap) (?R'11 rv') (KHeap_D.set_cap (transform_cslot_ptr p') (transform_cap cap)) (K_bind (CSpaceAcc_A.set_cap cap p') rv')
 2. \<lbrace>?Q11\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>\<lambda>old_cap s. old_cap = cdl_cap.NullCap \<and> ?P23 old_cap s\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> return () \<lbrace>?R'11\<rbrace>
 4. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and ?Q11 and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'11 and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. dcorres dc (?P23 cdl_cap.NullCap) (?R'11 ()) (KHeap_D.set_cap (transform_cslot_ptr p') (transform_cap cap)) (CSpaceAcc_A.set_cap cap p')
 2. \<lbrace>?Q11\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>\<lambda>old_cap s. old_cap = cdl_cap.NullCap \<and> ?P23 old_cap s\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> return () \<lbrace>?R'11\<rbrace>
 4. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and ?Q11 and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'11 and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<lbrace>?Q11\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>\<lambda>old_cap s. old_cap = cdl_cap.NullCap \<and> True\<rbrace>
 2. \<lbrace>?Q'11\<rbrace> return () \<lbrace>\<lambda>a b. valid_idle b \<and> fst p' \<noteq> idle_thread b \<and> valid_etcbs b\<rbrace>
 3. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and ?Q11 and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'11 and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. dcorres dc ?R4 ?R'4 (do y <- KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap;
modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))
od) (do y <- CSpaceAcc_A.set_cap cap.NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 2. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?R'4\<rbrace>
 4. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. dcorres dc ?P36 ?P'36 (KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap) (CSpaceAcc_A.set_cap cap.NullCap p)
 2. dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (do src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x. ?R36\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. ?R'36\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. ?P36 and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. ?P'36 and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (9 subgoals):
 1. cdl_cap.NullCap = transform_cap cap.NullCap
 2. transform_cslot_ptr p = transform_cslot_ptr p
 3. dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (do src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 4. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x. ?R36\<rbrace>
 5. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. ?R'36\<rbrace>
 6. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 9. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. transform_cslot_ptr p = transform_cslot_ptr p
 2. dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (do src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x. ?R36\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. ?R'36\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (do src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x. ?R36\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. ?R'36\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_p. dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (do dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x. ?R36\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. ?R'36\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_p dest_p. dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (do cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (cdt(p' := cdt p, p := None)) r = Some p then Some p' else (cdt(p' := cdt p, p := None)) r);
y <- cap_move_ext p p' src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original p' (is_original p);
set_original p False
od)
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x. ?R36\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. ?R'36\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_p dest_p. (p = p' \<longrightarrow> dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. cd))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := False)\<rparr>) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if r = p' then None else cdt s r\<rparr>)))) \<and> (p \<noteq> p' \<longrightarrow> dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p, p := False)\<rparr>) \<circ> ((\<lambda>s. cdt_list_update (\<lambda>_. (cdt_list s)(p := [], p' := cdt_list s p @ cdt_list s p')) s) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> cdt_list s | Some pa \<Rightarrow> (cdt_list s)(pa := list_replace (cdt_list s pa) p p')) s)) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if (if r = p then None else if r = p' then cdt s p else cdt s r) = Some p then Some p' else if r = p then None else if r = p' then cdt s p else cdt s r\<rparr>))))
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x. ?R36\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. ?R'36\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>dest_p. p = p' \<Longrightarrow> dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. cd))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := False)\<rparr>) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if r = p' then None else cdt s r\<rparr>)))
 2. \<And>src_p dest_p. p \<noteq> p' \<longrightarrow> dcorres dc ?R36 ?R'36 (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p, p := False)\<rparr>) \<circ> ((\<lambda>s. cdt_list_update (\<lambda>_. (cdt_list s)(p := [], p' := cdt_list s p @ cdt_list s p')) s) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> cdt_list s | Some pa \<Rightarrow> (cdt_list s)(pa := list_replace (cdt_list s pa) p p')) s)) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if (if r = p then None else if r = p' then cdt s p else cdt s r) = Some p then Some p' else if r = p then None else if r = p' then cdt s p else cdt s r\<rparr>)))
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x. ?R36\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. ?R'36\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>dest_p. p = p' \<Longrightarrow> dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')) (modify (cdl_cdt_update (\<lambda>cd. cd))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := False)\<rparr>) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if r = p' then None else cdt s r\<rparr>)))
 2. \<And>src_p dest_p. p \<noteq> p' \<longrightarrow> dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')) (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p, p := False)\<rparr>) \<circ> ((\<lambda>s. cdt_list_update (\<lambda>_. (cdt_list s)(p := [], p' := cdt_list s p @ cdt_list s p')) s) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> cdt_list s | Some pa \<Rightarrow> (cdt_list s)(pa := list_replace (cdt_list s pa) p p')) s)) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if (if r = p then None else if r = p' then cdt s p else cdt s r) = Some p then Some p' else if r = p then None else if r = p' then cdt s p else cdt s r\<rparr>)))
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>dest_p s s'. \<lbrakk>p = p'; True; (cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (cdl_cdt_update (\<lambda>cd. cd) s, ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := False)\<rparr>) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if r = p' then None else cdt s r\<rparr>)) s') \<in> {ss'. transform (snd ss') = fst ss'}
 2. \<And>src_p dest_p. p \<noteq> p' \<longrightarrow> dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')) (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p, p := False)\<rparr>) \<circ> ((\<lambda>s. cdt_list_update (\<lambda>_. (cdt_list s)(p := [], p' := cdt_list s p @ cdt_list s p')) s) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> cdt_list s | Some pa \<Rightarrow> (cdt_list s)(pa := list_replace (cdt_list s pa) p p')) s)) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if (if r = p then None else if r = p' then cdt s p else cdt s r) = Some p then Some p' else if r = p then None else if r = p' then cdt s p else cdt s r\<rparr>)))
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_p dest_p. p \<noteq> p' \<longrightarrow> dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')) (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p, p := False)\<rparr>) \<circ> ((\<lambda>s. cdt_list_update (\<lambda>_. (cdt_list s)(p := [], p' := cdt_list s p @ cdt_list s p')) s) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> cdt_list s | Some pa \<Rightarrow> (cdt_list s)(pa := list_replace (cdt_list s pa) p p')) s)) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if (if r = p then None else if r = p' then cdt s p else cdt s r) = Some p then Some p' else if r = p then None else if r = p' then cdt s p else cdt s r\<rparr>)))
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_p dest_p. p \<noteq> p' \<Longrightarrow> dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) (modify (cdl_cdt_update (\<lambda>cd. (\<lambda>x. if cd x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')))) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p, p := False)\<rparr>) \<circ> ((\<lambda>s. cdt_list_update (\<lambda>_. (cdt_list s)(p := [], p' := cdt_list s p @ cdt_list s p')) s) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> cdt_list s | Some pa \<Rightarrow> (cdt_list s)(pa := list_replace (cdt_list s pa) p p')) s)) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if (if r = p then None else if r = p' then cdt s p else cdt s r) = Some p then Some p' else if r = p then None else if r = p' then cdt s p else cdt s r\<rparr>)))
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_p dest_p s s'. \<lbrakk>p \<noteq> p'; True; (cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) 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 p) then Some (transform_cslot_ptr p') else if cd x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else cd x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')) s, ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p, p := False)\<rparr>) \<circ> ((\<lambda>s. cdt_list_update (\<lambda>_. (cdt_list s)(p := [], p' := cdt_list s p @ cdt_list s p')) s) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> cdt_list s | Some pa \<Rightarrow> (cdt_list s)(pa := list_replace (cdt_list s pa) p p')) s)) \<circ> (\<lambda>s. cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) p')) s) \<circ> (\<lambda>s. s\<lparr>cdt := \<lambda>r. if (if r = p then None else if r = p' then cdt s p else cdt s r) = Some p then Some p' else if r = p then None else if r = p' then cdt s p else cdt s r\<rparr>)) s') \<in> {ss'. transform (snd ss') = fst ss'}
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (\<lambda>r. if (if r = p then None else if r = p' then cdt s' p else cdt s' r) = Some p then Some p' else if r = p then None else if r = p' then cdt s' p else cdt s' r) = (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (\<lambda>r. if (if r = p then None else if r = p' then cdt s' p else cdt s' r) = Some p then Some p' else if r = p then None else if r = p' then cdt s' p else cdt s' r) = (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (\<lambda>r. if (if r = p then None else if r = p' then cdt s' p else cdt s' r) = Some p then Some p' else if r = p then None else if r = p' then cdt s' p else cdt s' r) = (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (9 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr (dom (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) \<union> ran (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) \<union> {p} \<union> set_option (Some p'))
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) x = Some (transform_cslot_ptr p) then map_option transform_cslot_ptr (Some p') else map_lift_over transform_cslot_ptr (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) x) = (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')
 3. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 4. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 6. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 9. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) x = Some (transform_cslot_ptr p) then map_option transform_cslot_ptr (Some p') else map_lift_over transform_cslot_ptr (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) x) = (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p')
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')); cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x) \<circ> Transposition.transpose (transform_cslot_ptr p) (transform_cslot_ptr p') = (\<lambda>x. if map_lift_over transform_cslot_ptr (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) x = Some (transform_cslot_ptr p) then map_option transform_cslot_ptr (Some p') else map_lift_over transform_cslot_ptr (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) x)
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr (insert p (insert p' (dom (cdt s') \<union> ran (cdt s')))); cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr p := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p') = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p') = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p'), transform_cslot_ptr p' := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p) = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p) = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p)) = (\<lambda>x. if map_lift_over transform_cslot_ptr (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else map_lift_over transform_cslot_ptr (\<lambda>r. if r = p then None else if r = p' then cdt s' p else cdt s' r) x)
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr (insert p (insert p' (dom (cdt s') \<union> ran (cdt s')))); cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> (\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr p := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p') = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p') = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p'), transform_cslot_ptr p' := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p) = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p) = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p)) = (\<lambda>x. if (if x = transform_cslot_ptr p then map_option transform_cslot_ptr None else if x = transform_cslot_ptr p' then map_option transform_cslot_ptr (cdt s' p) else map_lift_over transform_cslot_ptr (cdt s') x) = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if x = transform_cslot_ptr p then map_option transform_cslot_ptr None else if x = transform_cslot_ptr p' then map_option transform_cslot_ptr (cdt s' p) else map_lift_over transform_cslot_ptr (cdt s') x)
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s' x. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr (insert p (insert p' (dom (cdt s') \<union> ran (cdt s')))); cdt s' p \<noteq> Some p\<rbrakk> \<Longrightarrow> ((\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr p := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p') = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p') = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p'), transform_cslot_ptr p' := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p) = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p) = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p))) x = (if (if x = transform_cslot_ptr p then map_option transform_cslot_ptr None else if x = transform_cslot_ptr p' then map_option transform_cslot_ptr (cdt s' p) else map_lift_over transform_cslot_ptr (cdt s') x) = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if x = transform_cslot_ptr p then map_option transform_cslot_ptr None else if x = transform_cslot_ptr p' then map_option transform_cslot_ptr (cdt s' p) else map_lift_over transform_cslot_ptr (cdt s') x)
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>s' x a b aa ba. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr (insert p (insert p' (dom (cdt s') \<union> ran (cdt s')))); cdt s' p \<noteq> Some p; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> ((\<lambda>x. if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') x)(transform_cslot_ptr p := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p') = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p') = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p'), transform_cslot_ptr p' := if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p) = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p) = Some (transform_cslot_ptr p') then Some (transform_cslot_ptr p) else map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr p))) x = (if (if x = transform_cslot_ptr p then map_option transform_cslot_ptr None else if x = transform_cslot_ptr p' then map_option transform_cslot_ptr (cdt s' p) else map_lift_over transform_cslot_ptr (cdt s') x) = Some (transform_cslot_ptr p) then Some (transform_cslot_ptr p') else if x = transform_cslot_ptr p then map_option transform_cslot_ptr None else if x = transform_cslot_ptr p' then map_option transform_cslot_ptr (cdt s' p) else map_lift_over transform_cslot_ptr (cdt s') x)
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) 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'; cdt s' (aa, ba) = None; (aa, ba) \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (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); p = (a, b); p' = (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 (if x = transform_cslot_ptr (a, b) then None else if x = transform_cslot_ptr (aa, ba) then map_option transform_cslot_ptr (cdt s' (a, b)) else map_lift_over transform_cslot_ptr (cdt s') x) = Some (transform_cslot_ptr (a, b)) then Some (transform_cslot_ptr (aa, ba)) else if x = transform_cslot_ptr (a, b) then None else if x = transform_cslot_ptr (aa, ba) then map_option transform_cslot_ptr (cdt s' (a, b)) else map_lift_over transform_cslot_ptr (cdt s') x)
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) 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'; cdt s' (aa, ba) = None; (aa, ba) \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (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); p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> (x = transform_cslot_ptr (a, b) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None) \<and> x = transform_cslot_ptr (a, b)))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> (transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (x = transform_cslot_ptr (a, b) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None) \<and> x = transform_cslot_ptr (a, b))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (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))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (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))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> (transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (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))))))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (x = transform_cslot_ptr (a, b) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None) \<and> x = transform_cslot_ptr (a, b))))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') x \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> x = transform_cslot_ptr (a, b) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> (transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x = transform_cslot_ptr (a, b) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None)))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (a, b)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (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))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (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))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> (transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (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))))))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) \<noteq> Some (transform_cslot_ptr (a, b)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x = transform_cslot_ptr (a, b) \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (transform_cslot_ptr (aa, ba)) = None))))))
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) 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'; cdt s' (aa, ba) = None; (aa, ba) \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (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); p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)) \<longrightarrow> (transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (x = transform_cslot_ptr (a, b) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> x = transform_cslot_ptr (a, b)))))) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (a, b)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b)) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba)) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (x = transform_cslot_ptr (a, b) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> x = transform_cslot_ptr (a, b))))) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> map_option transform_cslot_ptr (cdt s' (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b))))) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> map_option transform_cslot_ptr (cdt s' (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b))))) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> map_option transform_cslot_ptr (cdt s' (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b))))))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b)) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba)) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (x = transform_cslot_ptr (a, b) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> x = transform_cslot_ptr (a, b))))))) \<and> (map_lift_over transform_cslot_ptr (cdt s') x \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)) \<longrightarrow> (transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> x = transform_cslot_ptr (a, b) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))))))) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (a, b)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (a, b)))))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x = transform_cslot_ptr (a, b) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba)))))) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<and> (transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> map_option transform_cslot_ptr (cdt s' (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b))))) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> map_option transform_cslot_ptr (cdt s' (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b))))) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))) \<and> (transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<and> ((\<forall>aa ba. cdt s' (a, b) = Some (aa, ba) \<longrightarrow> transform_cslot_ptr (aa, ba) \<noteq> transform_cslot_ptr (a, b)) \<longrightarrow> map_option transform_cslot_ptr (cdt s' (a, b)) = map_option transform_cslot_ptr (cdt s' (a, b))))))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> (Some (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (Some (transform_cslot_ptr (aa, ba)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> (Some (transform_cslot_ptr (a, b)) = map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> (Some (transform_cslot_ptr (a, b)) \<noteq> map_option transform_cslot_ptr (cdt s' (aa, ba)) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x = transform_cslot_ptr (a, b) \<longrightarrow> None = map_option transform_cslot_ptr (cdt s' (aa, ba))))))))
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) 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'; cdt s' (aa, ba) = None; (aa, ba) \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (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); p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> (map_lift_over transform_cslot_ptr (cdt s') x = Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> ((\<exists>ab bb. cdt s' (a, b) = Some (ab, bb) \<and> transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba)) \<longrightarrow> (aa = a \<and> ba = b \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>ba. cdt s' (a, b) = Some (a, ba) \<longrightarrow> ba \<noteq> b) \<and> ((\<forall>ba. cdt s' (a, b) = Some (a, ba) \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>aa ba. cdt s' (a, b) = Some (aa, ba) \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b)))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x = transform_cslot_ptr (a, b)))) \<and> ((\<forall>bb. cdt s' (a, b) = Some (aa, bb) \<longrightarrow> bb \<noteq> ba) \<longrightarrow> ((\<exists>aa ba. cdt s' (a, b) = Some (aa, ba) \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b)) \<longrightarrow> (x = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>ba. cdt s' (a, b) = Some (a, ba) \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>ab bb. cdt s' (a, b) = Some (ab, bb) \<and> transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba))) \<and> (x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x = transform_cslot_ptr (a, b))) \<and> ((\<forall>ba. cdt s' (a, b) = Some (a, ba) \<longrightarrow> ba \<noteq> b) \<longrightarrow> x \<noteq> transform_cslot_ptr (aa, ba) \<longrightarrow> x = transform_cslot_ptr (a, b)))) \<and> (map_lift_over transform_cslot_ptr (cdt s') x \<noteq> Some (transform_cslot_ptr (aa, ba)) \<longrightarrow> ((\<exists>ab bb. cdt s' (a, b) = Some (ab, bb) \<and> transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba)) \<longrightarrow> (aa = a \<and> ba = b \<longrightarrow> x \<noteq> transform_cslot_ptr (a, b)) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> x = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>ba. cdt s' (a, b) = Some (a, ba) \<longrightarrow> ba \<noteq> b) \<and> ((\<forall>ba. cdt s' (a, b) = Some (a, ba) \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>aa ba. cdt s' (a, b) = Some (aa, ba) \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b))))) \<and> ((\<forall>bb. cdt s' (a, b) = Some (aa, bb) \<longrightarrow> bb \<noteq> ba) \<longrightarrow> (\<exists>aa ba. cdt s' (a, b) = Some (aa, ba) \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b)) \<longrightarrow> x = transform_cslot_ptr (aa, ba) \<longrightarrow> (\<forall>ba. cdt s' (a, b) = Some (a, ba) \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>ab bb. cdt s' (a, b) = Some (ab, bb) \<and> transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba))))
 2. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 3. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 5. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 8. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p, p'} \<union> dom (cdt s') \<union> ran (cdt s')) \<and> cdt s' p \<noteq> Some p
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr (insert p (insert p' (dom (cdt s') \<union> ran (cdt s'))))
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>s' x. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s'; cte_wp_at (\<lambda>_. True) p' s'; cdt s' p' = None; p' \<notin> ran (cdt s'); no_mloop (cdt s'); mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); x \<in> insert p (insert p' (dom (cdt s') \<union> ran (cdt s')))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s'
 2. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 4. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q36\<rbrace> KHeap_D.set_cap (transform_cslot_ptr p) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrace>?Q'36\<rbrace> CSpaceAcc_A.set_cap cap.NullCap p \<lbrace>\<lambda>x. cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and (\<lambda>s. cdt s p' = None) and (\<lambda>s. p' \<notin> ran (cdt s)) and no_mloop \<circ> cdt and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s)) and K (p \<noteq> p')\<rbrace>
 3. \<lbrace>?Q4\<rbrace> insert_cap_orphan (transform_cap cap) (transform_cslot_ptr p') \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q36\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.set_cap cap p' \<lbrace>\<lambda>x. (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'36\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None) and (\<lambda>s. opt_cap (transform_cslot_ptr p') s \<noteq> None \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap \<and> True) and ?Q4) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'4) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>caps_of_state s' p' = Some cap.NullCap \<and> invs s' \<and> valid_etcbs s' \<and> (\<exists>cap. caps_of_state s' p = Some cap \<and> cap.NullCap \<noteq> cap) \<and> not_idle_thread (fst p') s' \<and> not_idle_thread (fst p) s'; transform s' = s\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (transform_cslot_ptr p') s = Some y) \<and> ((\<exists>y. opt_cap (transform_cslot_ptr p') s = Some y) \<longrightarrow> the (opt_cap (transform_cslot_ptr p') s) = cdl_cap.NullCap)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s \<and> cte_wp_at (\<lambda>_. True) p s \<and> cte_wp_at (\<lambda>_. True) p' s \<and> cdt s p' = None \<and> p' \<notin> ran (cdt s) \<and> no_mloop (cdt s) \<and> mdb_cte_at (\<lambda>y. \<exists>capa. ((caps_of_state s)(p' \<mapsto> cap, p \<mapsto> cap.NullCap)) y = Some capa) (cdt s) \<and> p \<noteq> p')) s' proof (prove)
goal (2 subgoals):
 1. \<And>s' cap. \<lbrakk>caps_of_state s' p' = Some cap.NullCap; invs s'; valid_etcbs s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'; caps_of_state s' p = Some cap; cap.NullCap \<noteq> cap\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (transform_cslot_ptr p') (transform s') = Some y) \<and> ((\<exists>y. opt_cap (transform_cslot_ptr p') (transform s') = Some y) \<longrightarrow> the (opt_cap (transform_cslot_ptr p') (transform s')) = cdl_cap.NullCap)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s \<and> cte_wp_at (\<lambda>_. True) p s \<and> cte_wp_at (\<lambda>_. True) p' s \<and> cdt s p' = None \<and> p' \<notin> ran (cdt s) \<and> no_mloop (cdt s) \<and> mdb_cte_at (\<lambda>y. \<exists>capa. ((caps_of_state s)(p' \<mapsto> cap, p \<mapsto> cap.NullCap)) y = Some capa) (cdt s) \<and> p \<noteq> p')) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>True; (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. valid_idle a \<and> fst p' \<noteq> idle_thread a \<and> valid_etcbs a) and (\<lambda>s. valid_idle s \<and> fst p \<noteq> idle_thread s \<and> valid_etcbs s \<and> cte_wp_at (\<lambda>_. True) p s \<and> cte_wp_at (\<lambda>_. True) p' s \<and> cdt s p' = None \<and> p' \<notin> ran (cdt s) \<and> no_mloop (cdt s) \<and> mdb_cte_at (\<lambda>y. \<exists>capa. ((caps_of_state s)(p' \<mapsto> cap, p \<mapsto> cap.NullCap)) y = Some capa) (cdt s) \<and> p \<noteq> p')) s' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>cte_wp_at ((=) cap.NullCap) p' s'; invs s'; valid_etcbs s'; cte_wp_at ((\<noteq>) cap.NullCap) p s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'\<rbrakk> \<Longrightarrow> valid_idle s' \<and> fst p' \<noteq> idle_thread s' \<and> valid_idle s' \<and> fst p \<noteq> idle_thread s' \<and> cte_wp_at (\<lambda>_. True) p s' \<and> cte_wp_at (\<lambda>_. True) p' s' \<and> p' \<notin> ran (cdt s') \<and> no_mloop (cdt s') \<and> mdb_cte_at (\<lambda>y. y \<noteq> p' \<longrightarrow> y \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s') \<and> p \<noteq> p' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>cte_wp_at ((=) cap.NullCap) p' s'; invs s'; valid_etcbs s'; cte_wp_at ((\<noteq>) cap.NullCap) p s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'; valid_mdb s'\<rbrakk> \<Longrightarrow> valid_idle s' \<and> fst p' \<noteq> idle_thread s' \<and> valid_idle s' \<and> fst p \<noteq> idle_thread s' \<and> cte_wp_at (\<lambda>_. True) p s' \<and> cte_wp_at (\<lambda>_. True) p' s' \<and> p' \<notin> ran (cdt s') \<and> no_mloop (cdt s') \<and> mdb_cte_at (\<lambda>y. y \<noteq> p' \<longrightarrow> y \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s') \<and> p \<noteq> p' proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>caps_of_state s' p' = Some cap.NullCap; invs s'; valid_etcbs s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); caps_of_state s' p = Some cap; cap.NullCap \<noteq> cap; 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> valid_idle s' \<and> fst p' \<noteq> idle_thread s' \<and> valid_idle s' \<and> fst p \<noteq> idle_thread s' \<and> p' \<notin> ran (cdt s') \<and> mdb_cte_at (\<lambda>y. y \<noteq> p' \<longrightarrow> y \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s') \<and> p \<noteq> p' proof (prove)
goal (6 subgoals):
 1. \<And>s' cap. \<lbrakk>caps_of_state s' p' = Some cap.NullCap; invs s'; valid_etcbs s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); caps_of_state s' p = Some cap; cap.NullCap \<noteq> cap; 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 p' = idle_thread s'\<rbrakk> \<Longrightarrow> False
 2. \<And>s' cap. \<lbrakk>caps_of_state s' p' = Some cap.NullCap; invs s'; valid_etcbs s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); caps_of_state s' p = Some cap; cap.NullCap \<noteq> cap; 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 p = idle_thread s'\<rbrakk> \<Longrightarrow> False
 3. \<And>s' cap. \<lbrakk>caps_of_state s' p' = Some cap.NullCap; invs s'; valid_etcbs s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); caps_of_state s' p = Some cap; cap.NullCap \<noteq> cap; 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'); p' \<in> ran (cdt s')\<rbrakk> \<Longrightarrow> False
 4. \<And>s' cap a b aa ba. \<lbrakk>caps_of_state s' p' = Some cap.NullCap; invs s'; valid_etcbs s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); caps_of_state s' p = Some cap; cap.NullCap \<noteq> cap; 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> p'; (aa, ba) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s' (aa, ba) = Some cap
 5. \<And>s' cap a b aa ba. \<lbrakk>caps_of_state s' p' = Some cap.NullCap; invs s'; valid_etcbs s'; not_idle_thread (fst p') s'; not_idle_thread (fst p) s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); caps_of_state s' p = Some cap; cap.NullCap \<noteq> cap; 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> p'; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s' (a, b) = Some cap
 6. \<And>s' cap. \<lbrakk>caps_of_state s' p' = Some cap.NullCap; invs s'; valid_etcbs s'; not_idle_thread (fst p') s'; not_idle_thread (fst p') s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); caps_of_state s' p' = Some cap; cap.NullCap \<noteq> cap; 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'); p = p'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres dc (\<lambda>_. True) (cte_wp_at ((=) cap.NullCap) p' and invs and valid_etcbs and cte_wp_at ((\<noteq>) cap.NullCap) p and not_idle_thread (fst p') and not_idle_thread (fst p)) (move_cap (transform_cap cap) (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_move cap p p')

goal:
No subgoals!