theory CNode_DR

lemma insert_cap_child_corres:
  "dcorres dc \<top>
        (\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s src)
                 cap (cap_insert_dest_original cap cap')) src s
              \<and> not_idle_thread (fst child) s \<and> valid_idle s \<and> valid_etcbs s
              \<and> valid_mdb s \<and> not_idle_thread (fst src) s \<and> valid_objs s \<and> cap_aligned cap)
        (insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr child))
        (cap_insert cap src child)" supply revokable_cap_insert_dest_original[simp] supply if_cong[cong] apply (simp add: cap_insert_def[folded cap_insert_dest_original_def]) apply (simp add: insert_cap_child_def insert_cap_orphan_def bind_assoc
                   option_return_modify_modify
                   gets_fold_into_modify update_cdt_modify
                   set_original_def modify_modify
                   cap_insert_ext_def update_cdt_list_def set_cdt_list_modify
             cong: option.case_cong) apply (rule stronger_corres_guard_imp) apply (rule corres_split[OF get_cap_corres], simp)+ apply (rule_tac P="old_cap \<noteq> cdl_cap.NullCap" and P'="rv' \<noteq> cap.NullCap"
          in corres_symmetric_bool_cases) apply (clarsimp simp :transform_cap_def split:cap.splits arch_cap.splits) apply (simp add:assert_def) apply (rule corres_trivial) apply (simp add:corres_free_fail) apply (simp add:assert_def) apply (rule corres_split[OF dcorres_set_untyped_cap_as_full]) apply (rule corres_split[OF set_cap_corres[OF refl refl]]) apply (rule dcorres_set_parent_helper) apply (rule_tac P=\<top> and P'="(\<lambda>s. should_be_parent_of src_capa (orig s) cap orig')
              and cte_at src and cte_at child
              and (\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s))" for orig orig'
              in corres_modify) apply (clarsimp split del: if_split) apply (subst if_P, assumption)+ apply (clarsimp simp: opt_parent_def transform_def transform_asid_table_def
                               transform_objects_def transform_cdt_def
                               transform_current_thread_def) apply (clarsimp simp: fun_upd_def[symmetric] cong:if_cong) apply (subgoal_tac "inj_on transform_cslot_ptr ({src, child} \<union> dom (cdt s') \<union> ran (cdt s'))") apply (subst map_lift_over_f_eq map_lift_over_upd,
                 erule subset_inj_on, fastforce)+ apply (simp add: fun_eq_iff) 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 get_cap_wp hoare_weak_lift_imp
                    | simp add: swp_def cte_wp_at_caps_of_state)+ apply (wp set_cap_idle |
          simp add:set_untyped_cap_as_full_def split del:if_split)+ apply (rule_tac Q = "\<lambda>r s. not_idle_thread (fst child) s
            \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa)
            \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
           in hoare_strengthen_post) apply (wp set_cap_mdb_cte_at | simp add:not_idle_thread_def)+ apply (clarsimp simp:mdb_cte_at_def cte_wp_at_caps_of_state) apply fastforce apply (wp get_cap_wp set_cap_idle hoare_weak_lift_imp
           | simp split del:if_split add:set_untyped_cap_as_full_def)+ apply (rule_tac Q = "\<lambda>r s. not_idle_thread (fst child) s
           \<and> (\<exists>cap. caps_of_state s src = Some cap)
           \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)
           \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
       in hoare_strengthen_post) apply (wp set_cap_mdb_cte_at hoare_weak_lift_imp | simp add:not_idle_thread_def)+ apply (clarsimp simp:mdb_cte_at_def cte_wp_at_caps_of_state) apply fastforce apply clarsimp apply (wp get_cap_wp |simp)+ apply (clarsimp simp: not_idle_thread_def) apply (clarsimp simp: caps_of_state_transform_opt_cap cte_wp_at_caps_of_state
    transform_cap_def)+ apply (clarsimp simp: valid_mdb_def cte_wp_at_cases dest!:invs_mdb) by (case_tac "cdt s' child", safe intro!: mdb_cte_atI;
         auto dest: mdb_cte_atD is_untyped_cap_eqD
              simp: valid_mdb_def swp_def cte_wp_at_caps_of_state not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s \<and> not_idle_thread (fst child) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst src) s \<and> valid_objs s \<and> cap_aligned cap) (insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr child)) (cap_insert cap src child) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s \<and> not_idle_thread (fst child) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst src) s \<and> valid_objs s \<and> cap_aligned cap) (insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr child)) (cap_insert cap src child) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s \<and> not_idle_thread (fst child) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst src) s \<and> valid_objs s \<and> cap_aligned cap) (insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr child)) (cap_insert cap src child) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s \<and> not_idle_thread (fst child) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst src) s \<and> valid_objs s \<and> cap_aligned cap) (insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr child)) (do src_cap <- CSpaceAcc_A.get_cap src;
old_cap <- CSpaceAcc_A.get_cap child;
y <- assert (old_cap = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_cap cap src;
y <- CSpaceAcc_A.set_cap cap child;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s child);
y <- update_cdt (\<lambda>cdt. cdt(child := if should_be_parent_of src_cap (is_original src) cap (cap_insert_dest_original cap src_cap) then Some src else cdt src));
y <- cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (cap_insert_dest_original cap src_cap)) src child src_p dest_p;
set_original child (cap_insert_dest_original cap src_cap)
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s \<and> not_idle_thread (fst child) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst src) s \<and> valid_objs s \<and> cap_aligned cap) (do src_cap <- KHeap_D.get_cap (transform_cslot_ptr src);
old_cap <- KHeap_D.get_cap (transform_cslot_ptr child);
y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do src_cap <- CSpaceAcc_A.get_cap src;
old_cap <- CSpaceAcc_A.get_cap child;
y <- assert (old_cap = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_cap cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_cap (is_original_cap s src) cap (cap_insert_dest_original cap src_cap) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_cap (is_original_cap s src) cap (cap_insert_dest_original cap src_cap) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_cap (is_original_cap s src) cap (cap_insert_dest_original cap src_cap) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_cap (is_original_cap s src) cap (cap_insert_dest_original cap src_cap) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_cap)\<rparr>)
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q19 ?Q'19 (do src_cap <- KHeap_D.get_cap (transform_cslot_ptr src);
old_cap <- KHeap_D.get_cap (transform_cslot_ptr child);
y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do src_cap <- CSpaceAcc_A.get_cap src;
old_cap <- CSpaceAcc_A.get_cap child;
y <- assert (old_cap = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_cap cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_cap (is_original_cap s src) cap (cap_insert_dest_original cap src_cap) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_cap (is_original_cap s src) cap (cap_insert_dest_original cap src_cap) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_cap (is_original_cap s src) cap (cap_insert_dest_original cap src_cap) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_cap (is_original_cap s src) cap (cap_insert_dest_original cap src_cap) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_cap)\<rparr>)
od)
 2. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q19 s
 3. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'19 s' proof (prove)
goal (7 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R29 src_cap src_capa old_cap) (?R'29 src_cap src_capa rv') (do y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- assert (rv' = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 2. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>?R29 src_cap src_capa\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>?R'29 src_cap src_capa\<rbrace>
 4. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 5. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 6. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (9 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'\<rbrakk> \<Longrightarrow> (old_cap \<noteq> cdl_cap.NullCap) = (rv' \<noteq> cap.NullCap)
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; old_cap \<noteq> cdl_cap.NullCap; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?Q39 src_cap src_capa old_cap) (?Q'41 src_cap src_capa rv') (do y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- assert (rv' = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 3. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; \<not> old_cap \<noteq> cdl_cap.NullCap; \<not> rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R40 src_cap src_capa old_cap) (?R'42 src_cap src_capa rv') (do y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- assert (rv' = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?Q39 src_cap src_capa old_cap s) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R40 src_cap src_capa old_cap s)\<rbrace>
 5. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> ?Q'41 src_cap src_capa rv' s) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> ?R'42 src_cap src_capa rv' s)\<rbrace>
 6. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 7. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 9. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (8 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; old_cap \<noteq> cdl_cap.NullCap; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?Q39 src_cap src_capa old_cap) (?Q'41 src_cap src_capa rv') (do y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- assert (rv' = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; \<not> old_cap \<noteq> cdl_cap.NullCap; \<not> rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R40 src_cap src_capa old_cap) (?R'42 src_cap src_capa rv') (do y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- assert (rv' = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?Q39 src_cap src_capa old_cap s) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R40 src_cap src_capa old_cap s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> ?Q'41 src_cap src_capa rv' s) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> ?R'42 src_cap src_capa rv' s)\<rbrace>
 5. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 6. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (8 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?Q39 (transform_cap src_capa) src_capa (transform_cap rv')) (?Q'41 (transform_cap src_capa) src_capa rv') fail fail
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; \<not> old_cap \<noteq> cdl_cap.NullCap; \<not> rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R40 src_cap src_capa old_cap) (?R'42 src_cap src_capa rv') (do y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- assert (rv' = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?Q39 src_cap src_capa old_cap s) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R40 src_cap src_capa old_cap s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> ?Q'41 src_cap src_capa rv' s) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> ?R'42 src_cap src_capa rv' s)\<rbrace>
 5. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 6. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (8 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) fail fail
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; \<not> old_cap \<noteq> cdl_cap.NullCap; \<not> rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R40 src_cap src_capa old_cap) (?R'42 src_cap src_capa rv') (do y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- assert (rv' = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R40 src_cap src_capa old_cap s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> ?R'42 src_cap src_capa rv' s)\<rbrace>
 5. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 6. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = transform_cap rv'; \<not> old_cap \<noteq> cdl_cap.NullCap; \<not> rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R40 src_cap src_capa old_cap) (?R'42 src_cap src_capa rv') (do y <- assert (old_cap = cdl_cap.NullCap);
y <- CSpace_D.set_untyped_cap_as_full src_cap (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- assert (rv' = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 2. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R40 src_cap src_capa old_cap s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> ?R'42 src_cap src_capa rv' s)\<rbrace>
 4. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 5. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 6. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R40 (transform_cap src_capa) src_capa cdl_cap.NullCap) (?R'42 (transform_cap src_capa) src_capa cap.NullCap) (do y <- CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src);
y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- CSpace_A.set_untyped_cap_as_full src_capa cap src;
y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 2. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R40 src_cap src_capa old_cap s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> ?R'42 src_cap src_capa rv' s)\<rbrace>
 4. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 5. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 6. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (9 subgoals):
 1. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R929 src_cap src_capa old_cap rv' y) (?R'929 src_cap src_capa old_cap rv' ya) (do y <- KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap);
set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)
od) (do y <- CSpaceAcc_A.set_cap cap child;
modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>)
od)
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>?R929 src_cap src_capa old_cap rv'\<rbrace>
 3. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>?R'929 src_cap src_capa old_cap rv'\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 5. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 6. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 7. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 9. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (11 subgoals):
 1. \<And>src_cap src_capa old_cap rv' y ya rv rv'a. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya; dc rv rv'a\<rbrakk> \<Longrightarrow> dcorres dc (?R942 src_cap src_capa old_cap rv' y ya rv) (?R'942 src_cap src_capa old_cap rv' y ya rv'a) (set_parent (transform_cslot_ptr child) (transform_cslot_ptr src)) (modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>))
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>?R942 src_cap src_capa old_cap rv' y ya\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>?R'942 src_cap src_capa old_cap rv' y ya\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_cap src_capa old_cap rv' y ya rv rv'a. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya; dc rv rv'a\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (?P955 src_cap src_capa old_cap rv' y ya rv'a) (modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr child \<mapsto> transform_cslot_ptr src)\<rparr>)) (modify (\<lambda>s. cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src) | Some p \<Rightarrow> (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child))(src := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src else (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p) src child else child # (case cdt s child of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) child)) p)) s)\<lparr>is_original_cap := (is_original_cap s)(child := cap_insert_dest_original cap src_capa)\<rparr>))
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ?P955 src_cap src_capa old_cap rv' y ya rv'a s\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_cap src_capa old_cap rv' y ya rv rv'a s s'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya; dc rv rv'a; True; ((\<lambda>s. should_be_parent_of src_capa (?orig962 src_cap src_capa old_cap rv' y ya rv'a s) cap (?orig'963 src_cap src_capa old_cap rv' y ya rv'a)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child 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> (s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr child \<mapsto> transform_cslot_ptr src)\<rparr>, cdt_update (\<lambda>cdt. cdt(child := if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src)) (cdt_list_update (\<lambda>_. case cdt s' src of None \<Rightarrow> (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child))(src := if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src else (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src) | Some p \<Rightarrow> (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child))(src := if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src else (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p) src child else child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p)) s')\<lparr>is_original_cap := (is_original_cap s')(child := cap_insert_dest_original cap src_capa)\<rparr>) \<in> {ss'. transform (snd ss') = fst ss'}
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (?orig962 src_cap src_capa old_cap rv' y ya rv'a s) cap (?orig'963 src_cap src_capa old_cap rv' y ya rv'a)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (?orig962 (transform_cap src_capa) src_capa cdl_cap.NullCap cap.NullCap () () () s') cap (?orig'963 (transform_cap src_capa) src_capa cdl_cap.NullCap cap.NullCap () () ()); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> transform (cdt_update (\<lambda>cdt a. if a = child then if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) then Some src else cdt src else cdt a) (cdt_list_update (\<lambda>_. case cdt s' src of None \<Rightarrow> (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child))(src := if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src else (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src) | Some p \<Rightarrow> (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child))(src := if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) then child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src else (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p) src child else child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p)) s')\<lparr>is_original_cap := \<lambda>a. if a = child then cap_insert_dest_original cap src_capa else is_original_cap s' a\<rparr>) = transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr child \<mapsto> transform_cslot_ptr src)\<rparr>
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (?orig962 src_cap src_capa old_cap rv' y ya rv'a s) cap (?orig'963 src_cap src_capa old_cap rv' y ya rv'a)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> transform (cdt_update (\<lambda>cdt a. if a = child then Some src else cdt a) (cdt_list_update (\<lambda>_. case cdt s' src of None \<Rightarrow> (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child))(src := child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src) | Some p \<Rightarrow> (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child))(src := child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) src, p := if should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa) \<and> p \<noteq> src then (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p else if src \<noteq> child then list_insert_after ((case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p) src child else child # (case cdt s' child of None \<Rightarrow> cdt_list s' | Some p \<Rightarrow> (cdt_list s')(p := list_remove (cdt_list s' p) child)) p)) s')\<lparr>is_original_cap := \<lambda>a. if a = child then cap_insert_dest_original cap src_capa else is_original_cap s' a\<rparr>) = transform s'\<lparr>cdl_cdt := (cdl_cdt (transform s'))(transform_cslot_ptr child \<mapsto> transform_cslot_ptr src)\<rparr>
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (\<lambda>a. if a = child then Some src else cdt s' a) = (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr child \<mapsto> transform_cslot_ptr src)
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr ((cdt s')(child \<mapsto> src)) = (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr child \<mapsto> transform_cslot_ptr src)
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr ({src, child} \<union> dom (cdt s') \<union> ran (cdt s'))\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr ((cdt s')(child \<mapsto> src)) = (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr child \<mapsto> transform_cslot_ptr src)
 2. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({src, child} \<union> dom (cdt s') \<union> ran (cdt s'))
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 6. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 8. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 9. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 10. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); inj_on transform_cslot_ptr ({src, child} \<union> dom (cdt s') \<union> ran (cdt s'))\<rbrakk> \<Longrightarrow> (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr child := map_option transform_cslot_ptr (Some src)) = (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr child \<mapsto> transform_cslot_ptr src)
 2. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({src, child} \<union> dom (cdt s') \<union> ran (cdt s'))
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 6. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 8. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 9. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 10. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_capa s'. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s')\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({src, child} \<union> dom (cdt s') \<union> ran (cdt s'))
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_capa s' x. \<lbrakk>should_be_parent_of src_capa (is_original_cap s' src) cap (cap_insert_dest_original cap src_capa); cte_wp_at (\<lambda>_. True) src s'; cte_wp_at (\<lambda>_. True) child s'; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); x \<in> {src, child} \<union> dom (cdt s') \<union> ran (cdt s')\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s'
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 5. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 7. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 8. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 9. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q946 src_cap src_capa old_cap rv' y\<rbrace> KHeap_D.set_cap (transform_cslot_ptr child) (transform_cap cap) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>src_cap src_capa old_cap rv' y ya. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'948 src_cap src_capa old_cap rv' ya\<rbrace> CSpaceAcc_A.set_cap cap child \<lbrace>\<lambda>rv'a s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ((\<lambda>s. should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)) and cte_wp_at (\<lambda>_. True) src and cte_wp_at (\<lambda>_. True) child and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s))) s\<rbrace>
 3. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q937 (transform_cap src_capa) src_capa cdl_cap.NullCap\<rbrace> CSpace_D.set_untyped_cap_as_full (transform_cap src_capa) (transform_cap cap) (transform_cslot_ptr src) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q946 src_cap src_capa old_cap rv' y\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'935 (transform_cap src_capa) src_capa cap.NullCap\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>ya. (\<lambda>s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'948 src_cap src_capa old_cap rv' ya\<rbrace>
 5. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and ?Q937 src_cap src_capa old_cap) s)\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and ?Q'935 src_cap src_capa rv') s)\<rbrace>
 7. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 8. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 9. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (8 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1169 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1164 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>rv s. src \<noteq> child \<longrightarrow> valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> ?P'1169 src_cap src_capa rv' a) \<and> ?P'1164 src_cap src_capa rv' a)) s)\<rbrace>
 5. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 6. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (9 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1205 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpaceAcc_A.set_cap (max_free_index_update src_capa) src \<lbrace>\<lambda>rv s. mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1174 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 3. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1164 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>rv s. src \<noteq> child \<longrightarrow> valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 5. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> ?P'1205 src_cap src_capa rv' a) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1174 src_cap src_capa rv' a)) \<and> ?P'1164 src_cap src_capa rv' a)) s)\<rbrace>
 6. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 7. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 9. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (10 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1205 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpaceAcc_A.set_cap (max_free_index_update src_capa) src \<lbrace>\<lambda>r s. not_idle_thread (fst child) s \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>src_cap src_capa old_cap rv' rv s. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap; not_idle_thread (fst child) s \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)
 3. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1174 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 4. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1164 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>rv s. src \<noteq> child \<longrightarrow> valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 5. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 6. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> ?P'1205 src_cap src_capa rv' a) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1174 src_cap src_capa rv' a)) \<and> ?P'1164 src_cap src_capa rv' a)) s)\<rbrace>
 7. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 8. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 9. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 10. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (9 subgoals):
 1. \<And>src_cap src_capa old_cap rv' s. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap; fst child \<noteq> idle_thread s \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1174 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 3. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1164 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>rv s. src \<noteq> child \<longrightarrow> valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 5. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1174 src_cap src_capa rv' a)) \<and> ?P'1164 src_cap src_capa rv' a)) s)\<rbrace>
 6. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 7. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 9. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (9 subgoals):
 1. \<And>src_capa s. \<lbrakk>Structures_A.is_untyped_cap src_capa; fst child \<noteq> idle_thread s; Structures_A.is_untyped_cap cap; should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap.NullCap \<noteq> cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> cap.NullCap \<noteq> cap); obj_ref_of src_capa = obj_ref_of cap; cap_bits_untyped src_capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> ((a, b) = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> ((aa, ba) = child \<longrightarrow> cap.NullCap \<noteq> cap)) \<and> (\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> ((a, b) \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap)) \<and> ((aa, ba) \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap)))
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1174 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 3. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1164 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>rv s. src \<noteq> child \<longrightarrow> valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 5. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1174 src_cap src_capa rv' a)) \<and> ?P'1164 src_cap src_capa rv' a)) s)\<rbrace>
 6. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 7. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 9. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (8 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1174 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1164 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpace_A.set_untyped_cap_as_full src_capa cap src \<lbrace>\<lambda>rv s. src \<noteq> child \<longrightarrow> valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1174 src_cap src_capa rv' a)) \<and> ?P'1164 src_cap src_capa rv' a)) s)\<rbrace>
 5. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 6. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (8 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1341 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpaceAcc_A.set_cap (max_free_index_update src_capa) src \<lbrace>\<lambda>rv s. mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1310 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. caps_of_state a child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt a) \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap)) (cdt a))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> ?P'1341 src_cap src_capa rv' a) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1310 src_cap src_capa rv' a)))) s)\<rbrace>
 5. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 6. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (9 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'1341 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> CSpaceAcc_A.set_cap (max_free_index_update src_capa) src \<lbrace>\<lambda>r s. not_idle_thread (fst child) s \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>src_cap src_capa old_cap rv' rv s. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap; not_idle_thread (fst child) s \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)
 3. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1310 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 5. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. caps_of_state a child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt a) \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap)) (cdt a))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> ?P'1341 src_cap src_capa rv' a) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1310 src_cap src_capa rv' a)))) s)\<rbrace>
 6. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 7. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 9. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (8 subgoals):
 1. \<And>src_cap src_capa old_cap rv' s. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap; fst child \<noteq> idle_thread s \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1310 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. caps_of_state a child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt a) \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap)) (cdt a))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) src = Some cap) \<and> should_be_parent_of src_capa (is_original_cap a src) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1310 src_cap src_capa rv' a)))) s)\<rbrace>
 5. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 6. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (8 subgoals):
 1. \<And>src_capa s capa. \<lbrakk>Structures_A.is_untyped_cap src_capa; fst child \<noteq> idle_thread s; Structures_A.is_untyped_cap cap; caps_of_state s src = Some capa; obj_ref_of src_capa = obj_ref_of cap; cap_bits_untyped src_capa = cap_bits_untyped cap; should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap.NullCap \<noteq> cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> cap.NullCap \<noteq> cap)\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> ((a, b) = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> ((aa, ba) = child \<longrightarrow> cap.NullCap \<noteq> cap)) \<and> (\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> ((a, b) \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap)) \<and> ((aa, ba) \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap)))
 2. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1310 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 4. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. caps_of_state a child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt a) \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap)) (cdt a))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) src = Some cap) \<and> should_be_parent_of src_capa (is_original_cap a src) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1310 src_cap src_capa rv' a)))) s)\<rbrace>
 5. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 6. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 8. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_cap src_capa old_cap rv'. \<lbrakk>src_cap = transform_cap src_capa; old_cap = cdl_cap.NullCap; rv' = cap.NullCap; \<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1310 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 2. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. caps_of_state a child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt a) \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap)) (cdt a))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) src = Some cap) \<and> should_be_parent_of src_capa (is_original_cap a src) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1310 src_cap src_capa rv' a)))) s)\<rbrace>
 4. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 5. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 6. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (7 subgoals):
 1. \<And>src_capa. obj_ref_of src_capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap src_capa \<longrightarrow> cap_bits_untyped src_capa \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>?R1310 (transform_cap src_capa) src_capa (ds_id cap.NullCap)\<rbrace> return () \<lbrace>\<lambda>rv s. valid_idle s \<and> fst child \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdt s child = None \<and> (\<exists>cap. caps_of_state s child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s) \<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa) \<and> (\<exists>cap. caps_of_state s src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s y = Some cap)) (cdt s)\<rbrace>
 2. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q31 src_cap\<rbrace> KHeap_D.get_cap (transform_cslot_ptr child) \<lbrace>\<lambda>old_cap s. (old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> True) \<and> (\<not> old_cap \<noteq> cdl_cap.NullCap \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s)\<rbrace>
 3. \<And>src_cap src_capa. src_cap = transform_cap src_capa \<Longrightarrow> \<lbrace>?Q'33 src_capa\<rbrace> CSpaceAcc_A.get_cap child \<lbrace>\<lambda>rv' s. (rv' \<noteq> cap.NullCap \<longrightarrow> True) \<and> (\<not> rv' \<noteq> cap.NullCap \<longrightarrow> (K (cap_aligned cap) and cte_wp_at ((=) src_capa) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs and (\<lambda>a. (src = child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. caps_of_state a child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt a) \<and> should_be_parent_of src_capa (is_original_cap a child) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state a y = Some cap)) (cdt a))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap \<longrightarrow> valid_idle a \<and> fst child \<noteq> idle_thread a \<and> valid_etcbs a \<and> cdt a child = None \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) child = Some cap) \<and> fst child \<noteq> idle_thread a \<and> (\<exists>cap. ((caps_of_state a)(src \<mapsto> max_free_index_update src_capa)) src = Some cap) \<and> should_be_parent_of src_capa (is_original_cap a src) cap (cap_insert_dest_original cap src_capa) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) a) (cdt a) \<and> (src \<in> dom (cdt a) \<union> ran (cdt a) \<longrightarrow> cap.NullCap \<noteq> max_free_index_update src_capa)) \<and> (\<not> (Structures_A.is_untyped_cap src_capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_capa = obj_ref_of cap \<and> cap_bits_untyped src_capa = cap_bits_untyped cap) \<longrightarrow> ?R1310 src_cap src_capa rv' a)))) s)\<rbrace>
 4. \<lbrace>?Q23\<rbrace> KHeap_D.get_cap (transform_cslot_ptr src) \<lbrace>\<lambda>src_cap. (\<lambda>_. True) and ?Q31 src_cap\<rbrace>
 5. \<lbrace>?Q'23\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>\<lambda>src_capa. valid_idle and not_idle_thread (fst child) and valid_etcbs and ?Q'33 src_capa\<rbrace>
 6. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q23) s
 7. \<And>s s'. \<lbrakk>True; cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst src) and valid_etcbs and ?Q'23) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s' \<and> not_idle_thread (fst child) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_mdb s' \<and> not_idle_thread (fst src) s' \<and> valid_objs s' \<and> cap_aligned cap; transform s' = s\<rbrakk> \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s' \<longrightarrow> cte_wp_at ((=) cap.NullCap) child s' \<longrightarrow> (src = child \<longrightarrow> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> fst child \<noteq> idle_thread s' \<and> cdt s' child = None \<and> fst child \<noteq> idle_thread s' \<and> should_be_parent_of capa (is_original_cap s' child) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s') \<and> (child \<in> dom (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa) \<and> (child \<in> ran (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> fst child \<noteq> idle_thread s' \<and> cdt s' child = None \<and> (\<exists>cap. caps_of_state s' child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s') \<and> should_be_parent_of capa (is_original_cap s' child) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s'))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> fst child \<noteq> idle_thread s' \<and> cdt s' child = None \<and> (\<exists>cap. caps_of_state s' child = Some cap) \<and> fst child \<noteq> idle_thread s' \<and> should_be_parent_of capa (is_original_cap s' src) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s') \<and> (src \<in> dom (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa) \<and> (src \<in> ran (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> fst child \<noteq> idle_thread s' \<and> cdt s' child = None \<and> (\<exists>cap. caps_of_state s' child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s') \<and> should_be_parent_of capa (is_original_cap s' src) cap (cap_insert_dest_original cap capa) \<and> (\<exists>cap. caps_of_state s' src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s' capa. \<lbrakk>cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'; fst child \<noteq> idle_thread s'; valid_idle s'; valid_etcbs s'; valid_mdb s'; fst src \<noteq> idle_thread s'; valid_objs s'; cap_aligned cap; cte_wp_at ((=) capa) src s'; cte_wp_at ((=) cap.NullCap) child s'\<rbrakk> \<Longrightarrow> (src = child \<longrightarrow> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> cdt s' child = None \<and> should_be_parent_of capa (is_original_cap s' child) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s') \<and> (child \<in> dom (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa) \<and> (child \<in> ran (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cdt s' child = None \<and> (\<exists>cap. caps_of_state s' child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s') \<and> should_be_parent_of capa (is_original_cap s' child) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s'))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> cdt s' child = None \<and> (\<exists>cap. caps_of_state s' child = Some cap) \<and> should_be_parent_of capa (is_original_cap s' src) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s') \<and> (src \<in> dom (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa) \<and> (src \<in> ran (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cdt s' child = None \<and> (\<exists>cap. caps_of_state s' child = Some cap) \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s') \<and> should_be_parent_of capa (is_original_cap s' src) cap (cap_insert_dest_original cap capa) \<and> (\<exists>cap. caps_of_state s' src = Some cap) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s' capa. \<lbrakk>should_be_parent_of capa (is_original_cap s' src) cap (cap_insert_dest_original cap capa); fst child \<noteq> idle_thread s'; valid_idle s'; valid_etcbs s'; valid_mdb s'; fst src \<noteq> idle_thread s'; valid_objs s'; cap_aligned cap; caps_of_state s' src = Some capa; caps_of_state s' child = Some cap.NullCap\<rbrakk> \<Longrightarrow> (src = child \<longrightarrow> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> cdt s' child = None \<and> should_be_parent_of capa (is_original_cap s' child) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>a. \<exists>cap. caps_of_state s' a = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s') \<and> (child \<in> dom (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa) \<and> (child \<in> ran (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cdt s' child = None \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s') \<and> should_be_parent_of capa (is_original_cap s' child) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s'))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> cdt s' child = None \<and> mdb_cte_at (\<lambda>a. \<exists>cap. caps_of_state s' a = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s') \<and> (src \<in> dom (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa) \<and> (src \<in> ran (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cdt s' child = None \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s') \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s' capa. \<lbrakk>should_be_parent_of capa (is_original_cap s' src) cap (cap_insert_dest_original cap capa); fst child \<noteq> idle_thread s'; valid_idle s'; valid_etcbs s'; fst src \<noteq> idle_thread s'; valid_objs s'; cap_aligned cap; caps_of_state s' src = Some capa; caps_of_state s' child = Some cap.NullCap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s')\<rbrakk> \<Longrightarrow> (src = child \<longrightarrow> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> cdt s' child = None \<and> should_be_parent_of capa (is_original_cap s' child) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>a. \<exists>cap. caps_of_state s' a = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s') \<and> (child \<in> dom (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa) \<and> (child \<in> ran (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cdt s' child = None \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s') \<and> should_be_parent_of capa (is_original_cap s' child) cap (cap_insert_dest_original cap capa) \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s'))) \<and> (src \<noteq> child \<longrightarrow> (Structures_A.is_untyped_cap capa \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> cdt s' child = None \<and> mdb_cte_at (\<lambda>a. \<exists>cap. caps_of_state s' a = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s') \<and> (src \<in> dom (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa) \<and> (src \<in> ran (cdt s') \<longrightarrow> cap.NullCap \<noteq> max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> Structures_A.is_untyped_cap cap \<longrightarrow> Structures_A.is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> cdt s' child = None \<and> mdb_cte_at (\<lambda>y. (y = child \<longrightarrow> cap.NullCap \<noteq> cap) \<and> (y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap))) (cdt s') \<and> mdb_cte_at (\<lambda>y. y \<noteq> child \<longrightarrow> (\<exists>cap. caps_of_state s' y = Some cap)) (cdt s')))