theory Finalise_DR

lemma dcorres_revoke_the_cap_corres:
  "dcorres dc \<top>
    (invs and cte_at slot and valid_etcbs)
    (revoke_cap_simple (transform_cslot_ptr slot))
    (do descs \<leftarrow> gets (CSpaceAcc_A.descendants_of slot \<circ> cdt);
        when (descs \<noteq> {}) (do y \<leftarrow> assert (\<exists>a b. descs = {(a, b)});
                          select descs >>= cap_delete_one
                          od)
    od)" supply if_cong[cong] apply (rule dcorres_revoke_cap_simple_helper) apply (simp add:gets_def) apply (rule dcorres_absorb_get_l) apply (rule dcorres_absorb_get_r) apply (subgoal_tac "finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'))") apply (clarsimp simp: finite_descendants_if_from_transform valid_mdb_def
                         invs_def valid_state_def descendants_of_eqv) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: when_def assert_def corres_free_fail) apply (subgoal_tac "cte_wp_at ((\<noteq>) cap.NullCap) (a,b) s'") prefer 2 apply (erule descendants_not_null_cap [rotated]) apply fastforce apply (rule conjI) prefer 2 apply (clarsimp simp: cte_wp_at_caps_of_state) apply (subgoal_tac "a \<noteq> idle_thread s'") apply (drule_tac p="(a,b)" in caps_of_state_transform_opt_cap) apply clarsimp apply clarsimp apply clarsimp apply clarsimp apply (erule notE, rule sym) apply (erule (4) valid_idle_has_null_cap) apply clarsimp apply (rule corres_dummy_return_r) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule delete_cap_simple_corres) apply (rule dcorres_revoke_cap_no_descendants) apply simp apply (wp cap_delete_one_cte_at)+ apply (rule_tac pres1 = s' and  p1 = slot in hoare_strengthen_post[OF delete_cap_one_shrink_descendants]) apply (simp_all add:invs_def valid_state_def valid_mdb_def) apply fastforce apply (rule conjI) apply (rule ccontr) apply (subgoal_tac "cte_wp_at ((\<noteq>)cap.NullCap) (a,b) s") apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule valid_idle_has_null_cap) apply (simp add:not_idle_thread_def)+ apply (rule invs_emptyable_descendants) apply (simp add:invs_def valid_state_def valid_mdb_def)+ apply (clarsimp simp:finite_descendants_if_from_transform) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) (revoke_cap_simple (transform_cslot_ptr slot)) (do descs <- gets (CSpaceAcc_A.descendants_of slot \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) (revoke_cap_simple (transform_cslot_ptr slot)) (do descs <- gets (CSpaceAcc_A.descendants_of slot \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) (do descendants <- gets $ KHeap_D.descendants_of (transform_cslot_ptr slot);
assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> opt_cap slot s \<noteq> None});
non_null_descendants <- return (descendants \<inter> non_null);
if non_null_descendants \<noteq> {} then do a <- select non_null_descendants;
y <- delete_cap_simple a;
revoke_cap_simple (transform_cslot_ptr slot)
od else return ()
od) (do descs <- gets (CSpaceAcc_A.descendants_of slot \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) (do s <- get;
y <- assert (finite (KHeap_D.descendants_of (transform_cslot_ptr slot) s));
sa <- get;
if KHeap_D.descendants_of (transform_cslot_ptr slot) s \<inter> {slot. opt_cap slot sa \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot sa = Some y)} \<noteq> {} then do a <- select (KHeap_D.descendants_of (transform_cslot_ptr slot) s \<inter> {slot. opt_cap slot sa \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot sa = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple (transform_cslot_ptr slot)
od else return ()
od) (do s <- get;
when (CSpaceAcc_A.descendants_of slot (cdt s) \<noteq> {}) (do y <- assert (\<exists>a b. CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)});
select (CSpaceAcc_A.descendants_of slot (cdt s)) >>= cap_delete_one
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')));
s <- get;
if KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)} \<noteq> {} then do a <- select (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple (transform_cslot_ptr slot)
od else return ()
od) (do s <- get;
when (CSpaceAcc_A.descendants_of slot (cdt s) \<noteq> {}) (do y <- assert (\<exists>a b. CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)});
select (CSpaceAcc_A.descendants_of slot (cdt s)) >>= cap_delete_one
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- assert (finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')));
s <- get;
if KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)} \<noteq> {} then do a <- select (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple (transform_cslot_ptr slot)
od else return ()
od) (when (CSpaceAcc_A.descendants_of slot (cdt s'a) \<noteq> {}) (do y <- assert (\<exists>a b. CSpaceAcc_A.descendants_of slot (cdt s'a) = {(a, b)});
select (CSpaceAcc_A.descendants_of slot (cdt s'a)) >>= cap_delete_one
od)) proof (prove)
goal (2 subgoals):
 1. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a; finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- assert (finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')));
s <- get;
if KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)} \<noteq> {} then do a <- select (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple (transform_cslot_ptr slot)
od else return ()
od) (when (CSpaceAcc_A.descendants_of slot (cdt s'a) \<noteq> {}) (do y <- assert (\<exists>a b. CSpaceAcc_A.descendants_of slot (cdt s'a) = {(a, b)});
select (CSpaceAcc_A.descendants_of slot (cdt s'a)) >>= cap_delete_one
od))
 2. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>finite (transform_cslot_ptr ` CSpaceAcc_A.descendants_of slot (cdt s'a)); valid_pspace s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); untyped_mdb (cdt s'a) (caps_of_state s'a); descendants_inc (cdt s'a) (caps_of_state s'a); no_mloop (cdt s'a); untyped_inc (cdt s'a) (caps_of_state s'a); ut_revocable (is_original_cap s'a) (caps_of_state s'a); irq_revocable (is_original_cap s'a) (caps_of_state s'a); reply_master_revocable (is_original_cap s'a) (caps_of_state s'a); reply_mdb (cdt s'a) (caps_of_state s'a); valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; cur_tcb s'a; cte_wp_at (\<lambda>_. True) slot s'a; valid_etcbs s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do s <- get;
if transform_cslot_ptr ` CSpaceAcc_A.descendants_of slot (cdt s'a) \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)} \<noteq> {} then do a <- select (transform_cslot_ptr ` CSpaceAcc_A.descendants_of slot (cdt s'a) \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple (transform_cslot_ptr slot)
od else return ()
od) (when (CSpaceAcc_A.descendants_of slot (cdt s'a) \<noteq> {}) (do y <- assert (\<exists>a b. CSpaceAcc_A.descendants_of slot (cdt s'a) = {(a, b)});
select (CSpaceAcc_A.descendants_of slot (cdt s'a)) >>= cap_delete_one
od))
 2. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (2 subgoals):
 1. \<And>s'a s'. \<lbrakk>finite (transform_cslot_ptr ` CSpaceAcc_A.descendants_of slot (cdt s'a)); valid_pspace s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); untyped_mdb (cdt s'a) (caps_of_state s'a); descendants_inc (cdt s'a) (caps_of_state s'a); no_mloop (cdt s'a); untyped_inc (cdt s'a) (caps_of_state s'a); ut_revocable (is_original_cap s'a) (caps_of_state s'a); irq_revocable (is_original_cap s'a) (caps_of_state s'a); reply_master_revocable (is_original_cap s'a) (caps_of_state s'a); reply_mdb (cdt s'a) (caps_of_state s'a); valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; cur_tcb s'a; cte_wp_at (\<lambda>_. True) slot s'a; valid_etcbs s'a; transform s'a = transform s'; s'a = s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (if transform_cslot_ptr ` CSpaceAcc_A.descendants_of slot (cdt s'a) \<inter> {slot. opt_cap slot (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot (transform s') = Some y)} \<noteq> {} then do a <- select (transform_cslot_ptr ` CSpaceAcc_A.descendants_of slot (cdt s'a) \<inter> {slot. opt_cap slot (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot (transform s') = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple (transform_cslot_ptr slot)
od else return ()) (when (CSpaceAcc_A.descendants_of slot (cdt s'a) \<noteq> {}) (do y <- assert (\<exists>a b. CSpaceAcc_A.descendants_of slot (cdt s'a) = {(a, b)});
select (CSpaceAcc_A.descendants_of slot (cdt s'a)) >>= cap_delete_one
od))
 2. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 2. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b. \<lbrakk>valid_pspace 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'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}\<rbrakk> \<Longrightarrow> (a, b) \<in> CSpaceAcc_A.descendants_of (?p71 s' a b) (cdt s')
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 2. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; caps_of_state s' (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (4 subgoals):
 1. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; caps_of_state s' (a, b) = Some capa; cap.NullCap \<noteq> capa; a \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 2. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; caps_of_state s' (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s'
 3. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 4. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (6 subgoals):
 1. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; cap.NullCap \<noteq> capa; a \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> valid_etcbs s'
 2. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; cap.NullCap \<noteq> capa; a \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> fst (a, b) \<noteq> idle_thread s'
 3. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; cap.NullCap \<noteq> capa; a \<noteq> idle_thread s'; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some (transform_cap capa)\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 4. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; caps_of_state s' (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s'
 5. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 6. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (5 subgoals):
 1. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; cap.NullCap \<noteq> capa; a \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> fst (a, b) \<noteq> idle_thread s'
 2. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; cap.NullCap \<noteq> capa; a \<noteq> idle_thread s'; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some (transform_cap capa)\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 3. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; caps_of_state s' (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s'
 4. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 5. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (4 subgoals):
 1. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; cap.NullCap \<noteq> capa; a \<noteq> idle_thread s'; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some (transform_cap capa)\<rbrakk> \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b))) \<and> (opt_cap (transform_cslot_ptr (a, b)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (cap_delete_one (a, b)))
 2. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; caps_of_state s' (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s'
 3. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 4. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; caps_of_state s' slot = Some cap; caps_of_state s' (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s'
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(idle_thread s', b)}; caps_of_state s' slot = Some cap; caps_of_state s' (idle_thread s', b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' b cap capa. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(idle_thread s', b)}; caps_of_state s' slot = Some cap; caps_of_state s' (idle_thread s', b) = Some capa\<rbrakk> \<Longrightarrow> capa = cap.NullCap
 2. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 3. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 2. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b))
 2. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b) >>= return)
 2. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (4 subgoals):
 1. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?Q111 s' a b y) (?Q'111 s' a b y) (do y <- delete_cap_simple (transform_cslot_ptr (a, b));
revoke_cap_simple (transform_cslot_ptr slot)
od) (cap_delete_one (a, b) >>= return)
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; transform s' = s\<rbrakk> \<Longrightarrow> ?Q111 s' a b y s
 3. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; s' = s\<rbrakk> \<Longrightarrow> ?Q'111 s' a b y s
 4. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (7 subgoals):
 1. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> dcorres (?r'115 s' a b y) (?P115 s' a b y) (?P'115 s' a b y) (delete_cap_simple (transform_cslot_ptr (a, b))) (cap_delete_one (a, b))
 2. \<And>s' a b y ya x. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; ?r'115 s' a b y ya x\<rbrakk> \<Longrightarrow> dcorres dc (?R115 s' a b y ya) (?R'115 s' a b y x) (revoke_cap_simple (transform_cslot_ptr slot)) (return x)
 3. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 s' a b y\<rbrace> delete_cap_simple (transform_cslot_ptr (a, b)) \<lbrace>?R115 s' a b y\<rbrace>
 4. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 s' a b y\<rbrace> cap_delete_one (a, b) \<lbrace>?R'115 s' a b y\<rbrace>
 5. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; transform s' = s\<rbrakk> \<Longrightarrow> (?P115 s' a b y and ?Q115 s' a b y) s
 6. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; s' = s\<rbrakk> \<Longrightarrow> (?P'115 s' a b y and ?Q'115 s' a b y) s
 7. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (6 subgoals):
 1. \<And>s' a b y ya x. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; dc ya x\<rbrakk> \<Longrightarrow> dcorres dc (?R115 s' a b y ya) (?R'115 s' a b y x) (revoke_cap_simple (transform_cslot_ptr slot)) (return x)
 2. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 s' a b y\<rbrace> delete_cap_simple (transform_cslot_ptr (a, b)) \<lbrace>?R115 s' a b y\<rbrace>
 3. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 s' a b y\<rbrace> cap_delete_one (a, b) \<lbrace>?R'115 s' a b y\<rbrace>
 4. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q115 s' a b y) s
 5. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; s' = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst (a, b)) and valid_etcbs and ?Q'115 s' a b y) s
 6. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (6 subgoals):
 1. \<And>s' a b y ya x. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; dc ya x\<rbrakk> \<Longrightarrow> transform_cslot_ptr slot = transform_cslot_ptr (?slot123 s' a b y x)
 2. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 s' a b y\<rbrace> delete_cap_simple (transform_cslot_ptr (a, b)) \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 s' a b y\<rbrace> cap_delete_one (a, b) \<lbrace>\<lambda>x s. valid_mdb s \<and> cte_wp_at (\<lambda>_. True) (?slot123 s' a b y x) s \<and> CSpaceAcc_A.descendants_of (?slot123 s' a b y x) (cdt s) = {}\<rbrace>
 4. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q115 s' a b y) s
 5. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; s' = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst (a, b)) and valid_etcbs and ?Q'115 s' a b y) s
 6. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (5 subgoals):
 1. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 s' a b y\<rbrace> delete_cap_simple (transform_cslot_ptr (a, b)) \<lbrace>\<lambda>ya _. True\<rbrace>
 2. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'115 s' a b y\<rbrace> cap_delete_one (a, b) \<lbrace>\<lambda>x s. valid_mdb s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> CSpaceAcc_A.descendants_of slot (cdt s) = {}\<rbrace>
 3. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q115 s' a b y) s
 4. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; s' = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst (a, b)) and valid_etcbs and ?Q'115 s' a b y) s
 5. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (4 subgoals):
 1. \<And>s' a b y. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?P'132 s' a b y\<rbrace> cap_delete_one (a, b) \<lbrace>\<lambda>rv s. CSpaceAcc_A.descendants_of slot (cdt s) = {}\<rbrace>
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 3. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; s' = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst (a, b)) and valid_etcbs and (\<lambda>s. (invs and emptyable (a, b)) s \<and> (invs and emptyable (a, b) and cte_wp_at (\<lambda>_. True) slot) s \<and> ?P'132 s' a b y s)) s
 4. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (4 subgoals):
 1. \<And>s' a b y rv s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; (a, b) \<notin> CSpaceAcc_A.descendants_of slot (cdt s) \<and> CSpaceAcc_A.descendants_of slot (cdt s) \<subseteq> CSpaceAcc_A.descendants_of slot (cdt s')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot (cdt s) = {}
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 3. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; s' = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst (a, b)) and valid_etcbs and (\<lambda>s. (invs and emptyable (a, b)) s \<and> (invs and emptyable (a, b) and cte_wp_at (\<lambda>_. True) slot) s \<and> s = s' \<and> invs s \<and> (a, b) \<in> CSpaceAcc_A.descendants_of slot (cdt s'))) s
 4. \<And>s' s'a. \<lbrakk>True; (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b y s. \<lbrakk>valid_pspace s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state s'); valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; cte_wp_at (\<lambda>_. True) slot s'; valid_etcbs s'; CSpaceAcc_A.descendants_of slot (cdt s') = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s'; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some y; (a, b) \<notin> CSpaceAcc_A.descendants_of slot (cdt s) \<and> CSpaceAcc_A.descendants_of slot (cdt s) \<subseteq> {(a, b)}\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot (cdt s) = {}
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> not_idle_thread a s \<and> emptyable (a, b) s
 3. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> not_idle_thread a s \<and> emptyable (a, b) s
 2. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> not_idle_thread a s
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> emptyable (a, b) s
 3. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s; \<not> not_idle_thread a s\<rbrakk> \<Longrightarrow> False
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> emptyable (a, b) s
 3. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (4 subgoals):
 1. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s; \<not> not_idle_thread a s; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s; \<not> not_idle_thread a s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s
 3. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> emptyable (a, b) s
 4. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (4 subgoals):
 1. \<And>a b y s cap capa. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; \<not> not_idle_thread a s; caps_of_state s slot = Some cap; caps_of_state s (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s; \<not> not_idle_thread a s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s
 3. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> emptyable (a, b) s
 4. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (8 subgoals):
 1. \<And>a b y s cap capa. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; \<not> not_idle_thread a s; caps_of_state s slot = Some cap; caps_of_state s (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> valid_global_refs s
 2. \<And>a b y s cap capa. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; \<not> not_idle_thread a s; caps_of_state s slot = Some cap; caps_of_state s (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> valid_idle s
 3. \<And>a b y s cap capa. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; \<not> not_idle_thread a s; caps_of_state s slot = Some cap; caps_of_state s (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> valid_irq_node s
 4. \<And>a b y s cap capa. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; \<not> not_idle_thread a s; caps_of_state s slot = Some cap; caps_of_state s (a, b) = Some capa; cap.NullCap \<noteq> capa\<rbrakk> \<Longrightarrow> caps_of_state s (idle_thread s, ?v175 a b y s cap capa) = Some (?cap175 a b y s cap capa)
 5. \<And>a b y s cap capa. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; \<not> not_idle_thread a s; caps_of_state s slot = Some cap; caps_of_state s (a, b) = Some capa; cap.NullCap \<noteq> capa; ?cap175 a b y s cap capa = cap.NullCap\<rbrakk> \<Longrightarrow> False
 6. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s; \<not> not_idle_thread a s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s
 7. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> emptyable (a, b) s
 8. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> emptyable (a, b) s
 2. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> invs s
 2. \<And>s' a b y s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) slot s; valid_etcbs s; CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}; cte_wp_at ((\<noteq>) cap.NullCap) (a, b) s; y \<noteq> cdl_cap.NullCap; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; s' = s\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of (?slot181 s' a b y s) (cdt s) = {(a, b)}
 3. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>valid_pspace s'a \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a) \<and> untyped_mdb (cdt s'a) (caps_of_state s'a) \<and> descendants_inc (cdt s'a) (caps_of_state s'a) \<and> no_mloop (cdt s'a) \<and> untyped_inc (cdt s'a) (caps_of_state s'a) \<and> ut_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> irq_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_master_revocable (is_original_cap s'a) (caps_of_state s'a) \<and> reply_mdb (cdt s'a) (caps_of_state s'a) \<and> valid_ioc s'a \<and> valid_idle s'a \<and> only_idle s'a \<and> if_unsafe_then_cap s'a \<and> valid_reply_caps s'a \<and> valid_reply_masters s'a \<and> valid_global_refs s'a \<and> valid_arch_state s'a \<and> valid_irq_node s'a \<and> valid_irq_handlers s'a \<and> valid_irq_states s'a \<and> valid_machine_state s'a \<and> valid_vspace_objs s'a \<and> valid_arch_caps s'a \<and> valid_global_objs s'a \<and> valid_kernel_mappings s'a \<and> equal_kernel_mappings s'a \<and> valid_asid_map s'a \<and> valid_global_vspace_mappings s'a \<and> pspace_in_kernel_window s'a \<and> cap_refs_in_kernel_window s'a \<and> pspace_respects_device_region s'a \<and> cap_refs_respects_device_region s'a \<and> cur_tcb s'a \<and> cte_wp_at (\<lambda>_. True) slot s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'a)) proof (prove)
goal:
No subgoals!