theory KHeap_DR

lemma delete_cap_simple_corres:
  "dcorres dc \<top> (invs and (not_idle_thread (fst slot)) and valid_etcbs)
             (delete_cap_simple (transform_cslot_ptr slot)) (cap_delete_one slot)" apply (clarsimp simp:delete_cap_simple_def cap_delete_one_def) apply (rule get_cap_no_fail) apply (rule corres_guard_imp) apply (rule_tac r'="%r r'. r = transform_cap r'" in corres_split) apply (rule get_cap_corres) apply simp apply (case_tac "rv' = cap.NullCap") apply (subgoal_tac "rv = cdl_cap.NullCap") apply (clarsimp simp:transform_cap_def unless_def when_def) apply (clarsimp simp:transform_cap_def) apply (subgoal_tac "rv\<noteq>cdl_cap.NullCap") apply (clarsimp simp:unless_def when_def) apply(rule corres_split[where r'="%x y. x=y"]) apply (subst is_final_cap_corres; simp) apply (rule corres_split[where r'="dc"]) apply simp apply (rule fast_finalise_corres) apply (rule always_empty_slot_corres) apply simp apply wp apply (rule hoare_post_imp [where Q="\<lambda>r. valid_mdb and valid_idle
                      and  not_idle_thread (fst slot) and valid_etcbs"]) apply (simp add:valid_mdb_def weak_valid_mdb_def) apply wp apply (wp|clarsimp)+ apply (clarsimp simp:transform_cap_def split:cap.splits arch_cap.splits if_split_asm) apply (clarsimp simp:not_idle_thread_def |wp get_cap_cte_wp_at_rv)+ apply (simp add:invs_def valid_state_def valid_pspace_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and not_idle_thread (fst slot) and valid_etcbs) (delete_cap_simple (transform_cslot_ptr slot)) (cap_delete_one slot) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and not_idle_thread (fst slot) and valid_etcbs) (do cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (transform_cslot_ptr slot)
od)
od) (do cap <- CSpaceAcc_A.get_cap slot;
unless (cap = cap.NullCap) (do final <- IpcCancel_A.is_final_cap cap;
y <- IpcCancel_A.fast_finalise cap final;
IpcCancel_A.empty_slot slot cap.NullCap
od)
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) (do cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (transform_cslot_ptr slot)
od)
od) (do cap <- CSpaceAcc_A.get_cap slot;
unless (cap = cap.NullCap) (do final <- IpcCancel_A.is_final_cap cap;
y <- IpcCancel_A.fast_finalise cap final;
IpcCancel_A.empty_slot slot cap.NullCap
od)
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q2 ?Q'2 (do cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (transform_cslot_ptr slot)
od)
od) (do cap <- CSpaceAcc_A.get_cap slot;
unless (cap = cap.NullCap) (do final <- IpcCancel_A.is_final_cap cap;
y <- IpcCancel_A.fast_finalise cap final;
IpcCancel_A.empty_slot slot cap.NullCap
od)
od)
 2. \<And>s. True \<Longrightarrow> ?Q2 s
 3. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. dcorres (\<lambda>r r'. r = transform_cap r') ?P6 ?P'6 (KHeap_D.get_cap (transform_cslot_ptr slot)) (CSpaceAcc_A.get_cap slot)
 2. \<And>rv rv'. rv = transform_cap rv' \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. transform_cslot_ptr slot = transform_cslot_ptr slot
 2. \<And>rv rv'. rv = transform_cap rv' \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. rv = transform_cap rv' \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 2. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 2. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' = cap.NullCap; rv = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 2. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> rv = cdl_cap.NullCap
 3. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 4. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' = cap.NullCap\<rbrakk> \<Longrightarrow> rv = cdl_cap.NullCap
 2. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 2. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap; rv \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (unless (rv = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap rv;
y <- PageTableUnmap_D.fast_finalise rv final;
always_empty_slot (transform_cslot_ptr slot)
od)) (unless (rv' = cap.NullCap) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od))
 2. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 (transform_cap rv')) (?R'6 rv') (do final <- PageTableUnmap_D.is_final_cap (transform_cap rv');
y <- PageTableUnmap_D.fast_finalise (transform_cap rv') final;
always_empty_slot (transform_cslot_ptr slot)
od) (do final <- IpcCancel_A.is_final_cap rv';
y <- IpcCancel_A.fast_finalise rv' final;
IpcCancel_A.empty_slot slot cap.NullCap
od)
 2. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (=) (?P19 (transform_cap rv')) (?P'15 rv') (PageTableUnmap_D.is_final_cap (transform_cap rv')) (IpcCancel_A.is_final_cap rv')
 2. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> dcorres dc (?R15 rv' final) (?R'15 rv' finala) (do y <- PageTableUnmap_D.fast_finalise (transform_cap rv') final;
always_empty_slot (transform_cslot_ptr slot)
od) (do y <- IpcCancel_A.fast_finalise rv' finala;
IpcCancel_A.empty_slot slot cap.NullCap
od)
 3. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>?R15 rv'\<rbrace>
 4. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>?R'15 rv'\<rbrace>
 5. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 6. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. ?P19 a and ?Q18 a\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. ?P'15 rv' and ?Q'15 rv'\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> dcorres dc (?R15 rv' final) (?R'15 rv' finala) (do y <- PageTableUnmap_D.fast_finalise (transform_cap rv') final;
always_empty_slot (transform_cslot_ptr slot)
od) (do y <- IpcCancel_A.fast_finalise rv' finala;
IpcCancel_A.empty_slot slot cap.NullCap
od)
 2. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>?R15 rv'\<rbrace>
 3. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>?R'15 rv'\<rbrace>
 4. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 5. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (11 subgoals):
 1. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> dcorres dc (?P34 rv' final) (?P'36 rv' finala) (PageTableUnmap_D.fast_finalise (transform_cap rv') final) (IpcCancel_A.fast_finalise rv' finala)
 2. \<And>rv' final finala rv rv'a. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala; dc rv rv'a\<rbrakk> \<Longrightarrow> dcorres dc (?R33 rv' final finala rv) (?R'33 rv' final finala rv'a) (always_empty_slot (transform_cslot_ptr slot)) (IpcCancel_A.empty_slot slot cap.NullCap)
 3. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 rv' final\<rbrace> PageTableUnmap_D.fast_finalise (transform_cap rv') final \<lbrace>?R33 rv' final finala\<rbrace>
 4. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 rv' finala\<rbrace> IpcCancel_A.fast_finalise rv' finala \<lbrace>?R'33 rv' final finala\<rbrace>
 5. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. ?P34 rv' final and ?Q35 rv' final\<rbrace>
 6. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. ?P'36 rv' finala and ?Q'37 rv' finala\<rbrace>
 7. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 8. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> dcorres dc (?P34 rv' finala) (?P'36 rv' finala) (PageTableUnmap_D.fast_finalise (transform_cap rv') finala) (IpcCancel_A.fast_finalise rv' finala)
 2. \<And>rv' final finala rv rv'a. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala; dc rv rv'a\<rbrakk> \<Longrightarrow> dcorres dc (?R33 rv' final finala rv) (?R'33 rv' final finala rv'a) (always_empty_slot (transform_cslot_ptr slot)) (IpcCancel_A.empty_slot slot cap.NullCap)
 3. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 rv' final\<rbrace> PageTableUnmap_D.fast_finalise (transform_cap rv') final \<lbrace>?R33 rv' final finala\<rbrace>
 4. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 rv' finala\<rbrace> IpcCancel_A.fast_finalise rv' finala \<lbrace>?R'33 rv' final finala\<rbrace>
 5. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. ?P34 rv' final and ?Q35 rv' final\<rbrace>
 6. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. ?P'36 rv' finala and ?Q'37 rv' finala\<rbrace>
 7. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 8. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv' final finala rv rv'a. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala; dc rv rv'a\<rbrakk> \<Longrightarrow> dcorres dc (?R33 rv' final finala rv) (?R'33 rv' final finala rv'a) (always_empty_slot (transform_cslot_ptr slot)) (IpcCancel_A.empty_slot slot cap.NullCap)
 2. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 rv' final\<rbrace> PageTableUnmap_D.fast_finalise (transform_cap rv') final \<lbrace>?R33 rv' final finala\<rbrace>
 3. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 rv' finala\<rbrace> IpcCancel_A.fast_finalise rv' finala \<lbrace>?R'33 rv' final finala\<rbrace>
 4. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. (\<lambda>_. True) and ?Q35 rv' final\<rbrace>
 5. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. valid_state and valid_idle and valid_etcbs and ?Q'37 rv' finala\<rbrace>
 6. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 7. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 rv' final\<rbrace> PageTableUnmap_D.fast_finalise (transform_cap rv') final \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 rv' finala\<rbrace> IpcCancel_A.fast_finalise rv' finala \<lbrace>\<lambda>rv'a. weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace>
 3. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. (\<lambda>_. True) and ?Q35 rv' final\<rbrace>
 4. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. valid_state and valid_idle and valid_etcbs and ?Q'37 rv' finala\<rbrace>
 5. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 6. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 rv' finala\<rbrace> IpcCancel_A.fast_finalise rv' finala \<lbrace>\<lambda>rv'a. weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace>
 2. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. (\<lambda>_. True) and ?Q35 rv' final\<rbrace>
 3. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. valid_state and valid_idle and valid_etcbs and ?Q'37 rv' finala\<rbrace>
 4. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 5. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 rv' finala\<rbrace> IpcCancel_A.fast_finalise rv' finala \<lbrace>\<lambda>rv'a s. weak_valid_mdb s \<and> valid_idle s \<and> not_idle_thread (fst slot) s \<and> valid_etcbs s\<rbrace>
 2. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. (\<lambda>_. True) and ?Q35 rv' final\<rbrace>
 3. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. valid_state and valid_idle and valid_etcbs and ?Q'37 rv' finala\<rbrace>
 4. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 5. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>rv' final finala rv s. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala; (valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s\<rbrakk> \<Longrightarrow> weak_valid_mdb s \<and> valid_idle s \<and> not_idle_thread (fst slot) s \<and> valid_etcbs s
 2. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 rv' finala\<rbrace> IpcCancel_A.fast_finalise rv' finala \<lbrace>\<lambda>r. valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace>
 3. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. (\<lambda>_. True) and ?Q35 rv' final\<rbrace>
 4. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. valid_state and valid_idle and valid_etcbs and ?Q'37 rv' finala\<rbrace>
 5. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 6. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>rv' final finala. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap; final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 rv' finala\<rbrace> IpcCancel_A.fast_finalise rv' finala \<lbrace>\<lambda>r. valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace>
 2. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. (\<lambda>_. True) and ?Q35 rv' final\<rbrace>
 3. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. valid_state and valid_idle and valid_etcbs and ?Q'37 rv' finala\<rbrace>
 4. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 5. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 (transform_cap rv')\<rbrace> PageTableUnmap_D.is_final_cap (transform_cap rv') \<lbrace>\<lambda>final. (\<lambda>_. True) and ?Q35 rv' final\<rbrace>
 2. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 rv'\<rbrace> IpcCancel_A.is_final_cap rv' \<lbrace>\<lambda>finala. valid_state and valid_idle and valid_etcbs and (\<lambda>s. invs s \<and> invs s \<and> not_idle_thread (fst slot) s \<and> valid_etcbs s)\<rbrace>
 3. \<And>rv rv'. \<lbrakk>rv = transform_cap rv'; rv' \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> rv \<noteq> cdl_cap.NullCap
 4. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q18 a\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and ?Q'15 rv'\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv'. \<lbrakk>rv' \<noteq> cap.NullCap; transform_cap rv' = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> False
 2. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>b. True \<and> K (?P80 a) b)\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and (valid_state and valid_idle and valid_etcbs and (\<lambda>s. invs s \<and> invs s \<and> not_idle_thread (fst slot) s \<and> valid_etcbs s))\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>b. True \<and> K (?P80 a) b)\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv'. valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs and (valid_state and valid_idle and valid_etcbs and (\<lambda>s. invs s \<and> invs s \<and> not_idle_thread (fst slot) s \<and> valid_etcbs s))\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 4. \<And>s. (invs and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; fst slot \<noteq> idle_thread s; valid_etcbs s; cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> valid_idle s \<and> valid_objs s \<and> valid_irq_node s \<and> valid_idle s \<and> if_unsafe_then_cap s \<and> valid_global_refs s \<and> valid_state s \<and> valid_idle s proof (prove)
goal:
No subgoals!