theory Tcb_IF

lemma rec_del_preservation2':
  assumes finalise_cap_P: "\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>"
  assumes set_cap_P: "\<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>"
  assumes set_cap_Q: "\<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>"
  assumes empty_slot_P: "\<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>"
  assumes empty_slot_Q: "\<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>"
  assumes cap_swap_for_delete_Q: "\<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>"
  assumes cap_swap_for_delete_P: "\<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>"
  assumes preemption_point_Q: "\<And>a b. \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>"
  assumes preemption_point_P: "\<And>a b. \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>"
  assumes invs_Q: "\<And>s. invs s \<Longrightarrow> Q s"
  assumes invs_R: "\<And>s slot cap. invs s \<Longrightarrow> caps_of_state s slot = Some cap \<Longrightarrow> R cap s"
  shows "s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace>
             rec_del call
             \<lbrace>\<lambda>rv s :: det_state. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>" proof (induct rule: rec_del.induct, simp_all only: rec_del_fails) case (1 slot exposed s) show ?case apply (subst rec_del.simps) apply (simp only: split_def) apply (rule hoare_pre_spec_validE) apply (rule split_spec_bindE) apply (wp empty_slot_P empty_slot_Q)[1] apply (rule spec_strengthen_postE) apply (rule "1.hyps") apply auto done next case (2 slot exposed s) show ?case apply (subst rec_del.simps) apply (simp only: split_def) apply (rule hoare_pre_spec_validE) apply wp apply (wp set_cap_P set_cap_Q "2.hyps")+ apply ((wp preemption_point_Q preemption_point_P preemption_point_inv | simp)+)[1] apply (simp(no_asm)) apply (rule spec_strengthen_postE) apply (rule spec_valid_conj_liftE1, rule valid_validE_R, rule rec_del_invs) apply (rule spec_valid_conj_liftE1, rule reduce_zombie_cap_to) apply (rule spec_valid_conj_liftE1, rule rec_del_emptyable) apply (rule "2.hyps") apply simp apply (simp add: conj_comms) apply (wp set_cap_P set_cap_Q replace_cap_invs
                        final_cap_same_objrefs set_cap_cte_cap_wp_to
                        set_cap_cte_wp_at hoare_vcg_const_Ball_lift hoare_weak_lift_imp
                     | rule finalise_cap_not_reply_master
                     | simp add: in_monad)+ apply (rule hoare_strengthen_post) apply (rule_tac Q="\<lambda>fin s. invs s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> (fst fin)
                                          \<and> P s
                                          \<and> replaceable s slot (fst fin) rv
                                          \<and> emptyable slot s
                                          \<and> (\<forall>t\<in>obj_refs_ac (fst fin). halted_if_tcb t s)
                                          \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s"
                     in hoare_vcg_conj_lift) apply (wp finalise_cap_invs[where slot=slot]
                   finalise_cap_replaceable[where sl=slot]
                   Finalise_AC_1.finalise_cap_makes_halted[where slot=slot]
                   finalise_cap_P)[1] apply (rule finalise_cap_cases[where slot=slot]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule invs_valid_global_objs) apply (frule invs_Q) apply (erule disjE) apply clarsimp apply (clarsimp simp: is_cap_simps cap_auth_conferred_def clas_no_asid aag_cap_auth_def
                             pas_refined_all_auth_is_owns cli_no_irqs gen_obj_refs_eq) apply (drule appropriate_Zombie[symmetric, THEN trans, symmetric]) apply clarsimp apply (erule_tac s = "{r}" in subst) apply simp apply (simp add: is_final_cap_def) apply wp apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state conj_comms) apply (frule (1) caps_of_state_valid) apply (clarsimp simp: conj_comms invs_def valid_state_def valid_pspace_def invs_R) apply (frule if_unsafe_then_capD [OF caps_of_state_cteD],clarsimp+) done next case (3 ptr bits n slot s) show ?case apply (simp add: spec_validE_def) apply (rule hoare_pre, wp cap_swap_for_delete_P cap_swap_for_delete_Q) apply (clarsimp) done next case (4 ptr bits n slot s) show ?case apply (subst rec_del.simps) apply (rule hoare_pre_spec_validE) apply (rule split_spec_bindE) apply (rule split_spec_bindE[rotated]) apply (rule "4.hyps", assumption+) apply (wp set_cap_P set_cap_Q get_cap_wp | simp) apply simp apply simp apply wp apply (clarsimp simp add: zombie_is_cap_toE) apply (clarsimp simp: cte_wp_at_caps_of_state zombie_ptr_emptyable) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (state)
goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s \<and> valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) s\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s \<and> valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) s\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s\<rbrace> doE p <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> fst p) $ empty_slot slot (snd p);
returnOk undefined
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> doE p <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> fst p) $ empty_slot slot (snd p);
returnOk undefined
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (rec_del (FinaliseSlotCall slot exposed) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B3 rv\<rbrace> doE without_preemption $ when (exposed \<or> fst rv) $ empty_slot slot (snd rv);
returnOk undefined
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. s \<turnstile> \<lbrace>?P'\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then \<lambda>a. (Q and P) a \<and> Q a else (\<lambda>a. P a \<and> Q a)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>?Q'25\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>s r. ?Q'25 s r \<Longrightarrow> (if exposed \<or> fst s then \<lambda>a. (Q and P) a \<and> Q a else (\<lambda>a. P a \<and> Q a)) r
 3. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<And>s r. P r \<and> Q r \<Longrightarrow> (if exposed \<or> fst s then \<lambda>a. (Q and P) a \<and> Q a else (\<lambda>a. P a \<and> Q a)) r
 2. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s \<Longrightarrow> invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall slot exposed)) s \<and> valid_rec_del_call (CTEDeleteCall slot exposed) s\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s \<and> valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) s\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (state)
goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s \<and> valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) s\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap slot) s); ?rv \<noteq> NullCap; (Inr ?rva, ?sta) \<in> fst ((without_preemption $ is_final_cap ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst ((without_preemption $ finalise_cap ?rv ?rva) ?sta); \<not> cap_removeable (fst ?rvb) slot; \<not> (cap_cyclic_zombie (fst ?rvb) slot \<and> \<not> exposed); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) slot) ?stb)\<rbrakk> \<Longrightarrow> ?stc \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (fst ?rvb) slot exposed)) s \<and> valid_rec_del_call (ReduceZombieCall (fst ?rvb) slot exposed) s\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap slot) s); ?rv \<noteq> NullCap; (Inr ?rva, ?sta) \<in> fst ((without_preemption $ is_final_cap ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst ((without_preemption $ finalise_cap ?rv ?rva) ?sta); \<not> cap_removeable (fst ?rvb) slot; \<not> (cap_cyclic_zombie (fst ?rvb) slot \<and> \<not> exposed); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) slot) ?stb); (Inr ?rvd, ?std) \<in> fst (rec_del (ReduceZombieCall (fst ?rvb) slot exposed) ?stc); (Inr ?rve, ?ste) \<in> fst (preemption_point ?std)\<rbrakk> \<Longrightarrow> ?ste \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s \<and> valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) s\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst ((without_preemption $ is_final_cap rv) st); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> doE cap <- without_preemption $ get_cap slot;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
(remainder, cleanup_info) <- without_preemption $ finalise_cap cap is_final;
if cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> exposed then doE without_preemption $ set_cap remainder slot;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> doE cap <- without_preemption $ get_cap slot;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
p <- without_preemption $ finalise_cap cap is_final;
if cap_removeable (fst p) slot then returnOk (True, snd p) else if cap_cyclic_zombie (fst p) slot \<and> \<not> exposed then doE without_preemption $ set_cap (fst p) slot;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap (fst p) slot;
rec_del (ReduceZombieCall (fst p) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> doE cap <- without_preemption $ get_cap slot;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
p <- without_preemption $ finalise_cap cap is_final;
if cap_removeable (fst p) slot then returnOk (True, snd p) else if cap_cyclic_zombie (fst p) slot \<and> \<not> exposed then doE without_preemption $ set_cap (fst p) slot;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap (fst p) slot;
rec_del (ReduceZombieCall (fst p) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?P23 rv s'' rva s''a rvb\<rbrace> set_cap (fst rvb) slot \<lbrace>\<lambda>a b. P b \<and> Q b\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> doE without_preemption $ set_cap (fst rvb) slot;
rec_del (ReduceZombieCall (fst rvb) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> ?P23 rv s'' rva s''a rvb s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c)\<rbrakk> \<Longrightarrow> \<lbrace>?B44 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>\<lambda>rve s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B42 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B44 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B42 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 7. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B42 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd s. (Q and P) s \<and> Q s \<and> invs s \<and> (Q and P) s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B42 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B42 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd s. Q s \<and> P s \<and> Q s \<and> invs s \<and> Q s \<and> P s \<and> Q s \<and> emptyable slot s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B42 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B42 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?Q'81 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); ?Q'81 rv s'' rva s''a rvb s''b rvc s''c s r\<rbrakk> \<Longrightarrow> Q r \<and> P r \<and> Q r \<and> invs r \<and> Q r \<and> P r \<and> Q r \<and> emptyable slot r
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B42 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 7. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'86 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?Q'85 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); invs r \<and> ?Q'85 rv s'' rva s''a rvb s''b rvc s''c s r\<rbrakk> \<Longrightarrow> Q r \<and> P r \<and> Q r \<and> invs r \<and> Q r \<and> P r \<and> Q r \<and> emptyable slot r
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>a aa. (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) aa \<and> ?P'86 rv s'' rva s''a rvb s''b a aa\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 7. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'98 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?Q'97 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); invs r \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot r) \<and> ?Q'97 rv s'' rva s''a rvb s''b rvc s''c s r\<rbrakk> \<Longrightarrow> Q r \<and> P r \<and> Q r \<and> invs r \<and> Q r \<and> P r \<and> Q r \<and> emptyable slot r
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>a aa. (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) aa \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable (fst rvb) slot) and (\<lambda>s. \<forall>t\<in>obj_refs (fst rvb). halted_if_tcb t s)) aa \<and> ?P'98 rv s'' rva s''a rvb s''b a aa\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 7. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'106 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?Q'105 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); invs r \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot r) \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) r \<and> ?Q'105 rv s'' rva s''a rvb s''b rvc s''c s r\<rbrakk> \<Longrightarrow> Q r \<and> P r \<and> Q r \<and> invs r \<and> Q r \<and> P r \<and> Q r \<and> emptyable slot r
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>a aa. (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) aa \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable (fst rvb) slot) and (\<lambda>s. \<forall>t\<in>obj_refs (fst rvb). halted_if_tcb t s)) aa \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) aa \<and> ?P'106 rv s'' rva s''a rvb s''b a aa\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 7. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (13 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr (?rv113 rv s'' rva s''a rvb s''b rvc s''c), ?st113 rv s'' rva s''a rvb s''b rvc s''c) \<in> fst ((without_preemption $ get_cap slot) s)
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> ?rv113 rv s'' rva s''a rvb s''b rvc s''c \<noteq> NullCap
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr (?rva113 rv s'' rva s''a rvb s''b rvc s''c), ?sta113 rv s'' rva s''a rvb s''b rvc s''c) \<in> fst ((without_preemption $ is_final_cap (?rv113 rv s'' rva s''a rvb s''b rvc s''c)) (?st113 rv s'' rva s''a rvb s''b rvc s''c))
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr rvb, ?stb113 rv s'' rva s''a rvb s''b rvc s''c) \<in> fst ((without_preemption $ finalise_cap (?rv113 rv s'' rva s''a rvb s''b rvc s''c) (?rva113 rv s'' rva s''a rvb s''b rvc s''c)) (?sta113 rv s'' rva s''a rvb s''b rvc s''c))
 5. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> \<not> cap_removeable (fst rvb) slot
 6. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)
 7. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr (?rvc113 rv s'' rva s''a rvb s''b rvc s''c), s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) (?stb113 rv s'' rva s''a rvb s''b rvc s''c))
 8. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); invs r \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot r) \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) r \<and> P r \<and> Q r\<rbrakk> \<Longrightarrow> Q r \<and> P r \<and> Q r \<and> invs r \<and> Q r \<and> P r \<and> Q r \<and> emptyable slot r
 9. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>a b. (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) b \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable (fst rvb) slot) and (\<lambda>s. \<forall>t\<in>obj_refs (fst rvb). halted_if_tcb t s)) b \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) b \<and> invs b \<and> P b \<and> Q b \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) b \<and> valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) b\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 10. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> rv \<noteq> NullCap
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr (?rva113 rv s'' rva s''a rvb s''b rvc s''c), ?sta113 rv s'' rva s''a rvb s''b rvc s''c) \<in> fst ((without_preemption $ is_final_cap rv) s'')
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr rvb, ?stb113 rv s'' rva s''a rvb s''b rvc s''c) \<in> fst ((without_preemption $ finalise_cap rv (?rva113 rv s'' rva s''a rvb s''b rvc s''c)) (?sta113 rv s'' rva s''a rvb s''b rvc s''c))
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> \<not> cap_removeable (fst rvb) slot
 5. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)
 6. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr (?rvc113 rv s'' rva s''a rvb s''b rvc s''c), s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) (?stb113 rv s'' rva s''a rvb s''b rvc s''c))
 7. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); invs r \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot r) \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) r \<and> P r \<and> Q r\<rbrakk> \<Longrightarrow> Q r \<and> P r \<and> Q r \<and> invs r \<and> Q r \<and> P r \<and> Q r \<and> emptyable slot r
 8. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>a b. (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) b \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable (fst rvb) slot) and (\<lambda>s. \<forall>t\<in>obj_refs (fst rvb). halted_if_tcb t s)) b \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) b \<and> invs b \<and> P b \<and> Q b \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) b \<and> valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) b\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 9. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 10. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr (?rva113 rv s'' rva s''a rvb s''b rvc s''c), ?sta113 rv s'' rva s''a rvb s''b rvc s''c) \<in> fst ((without_preemption $ is_final_cap rv) s'')
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr rvb, ?stb113 rv s'' rva s''a rvb s''b rvc s''c) \<in> fst ((without_preemption $ finalise_cap rv (?rva113 rv s'' rva s''a rvb s''b rvc s''c)) (?sta113 rv s'' rva s''a rvb s''b rvc s''c))
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> \<not> cap_removeable (fst rvb) slot
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)
 5. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> (Inr (?rvc113 rv s'' rva s''a rvb s''b rvc s''c), s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) (?stb113 rv s'' rva s''a rvb s''b rvc s''c))
 6. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); invs r \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot r) \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) r \<and> P r \<and> Q r\<rbrakk> \<Longrightarrow> Q r \<and> P r \<and> Q r \<and> invs r \<and> Q r \<and> P r \<and> Q r \<and> emptyable slot r
 7. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>a b. (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) b \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable (fst rvb) slot) and (\<lambda>s. \<forall>t\<in>obj_refs (fst rvb). halted_if_tcb t s)) b \<and> (invs and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and (\<lambda>s. \<not> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) s) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and (\<lambda>s. case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) b \<and> invs b \<and> P b \<and> Q b \<and> emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) b \<and> valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) b\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 8. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (Q and P) s \<and> Q s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'25 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 9. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 10. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B12 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> Q s \<and> P s \<and> Q s) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> Q s \<and> P s \<and> Q s \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb)))\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B12 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q339 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); ?Q339 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> Q s \<and> P s \<and> Q s) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> Q s \<and> P s \<and> Q s \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb)))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P344 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>fin s. invs s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> fst fin \<and> P s \<and> replaceable s slot (fst fin) rv \<and> emptyable slot s \<and> (\<forall>t\<in>obj_refs_ac (fst fin). halted_if_tcb t s) \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'345 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q'342 rv s'' rva s''a\<rbrace>
 3. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (invs s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> fst rvb \<and> P s \<and> replaceable s slot (fst rvb) rv \<and> emptyable slot s \<and> (\<forall>t\<in>obj_refs_ac (fst rvb). halted_if_tcb t s) \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> ?Q'342 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> Q s \<and> P s \<and> Q s) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> Q s \<and> P s \<and> Q s \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb)))
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ?P344 rv s'' rva s \<and> ?P'345 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 6. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'345 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q'342 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (invs s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> fst rvb \<and> P s \<and> replaceable s slot (fst rvb) rv \<and> emptyable slot s \<and> (\<forall>t\<in>obj_refs_ac (fst rvb). halted_if_tcb t s) \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> ?Q'342 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> Q s \<and> P s \<and> Q s) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> Q s \<and> P s \<and> Q s \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb)))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> ?P'345 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (invs s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> fst rvb \<and> P s \<and> replaceable s slot (fst rvb) rv \<and> emptyable slot s \<and> (\<forall>t\<in>obj_refs_ac (fst rvb). halted_if_tcb t s) \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (fst rvb = NullCap \<and> snd rvb = (if rva then cap_cleanup_opt rv else NullCap) \<and> (snd rvb \<noteq> NullCap \<longrightarrow> is_final_cap' rv s) \<or> is_zombie (fst rvb) \<and> is_final_cap' rv s \<and> is_final_cap' (fst rvb) s \<and> snd rvb = NullCap \<and> appropriate_cte_cap (fst rvb) = appropriate_cte_cap rv \<and> cte_refs (fst rvb) = cte_refs rv \<and> gen_obj_refs (fst rvb) = gen_obj_refs rv \<and> obj_size (fst rvb) = obj_size rv \<and> fst_cte_ptrs (fst rvb) = fst_cte_ptrs rv \<and> vs_cap_ref rv = None)\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> P s \<and> Q s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> Q s \<and> P s \<and> Q s) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> Q s \<and> P s \<and> Q s \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb)))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a a b s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> a; P s; replaceable s slot a rv; emptyable slot s; \<forall>t\<in>obj_refs_ac a. halted_if_tcb t s; ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s; a = NullCap \<and> b = (if rva then cap_cleanup_opt rv else NullCap) \<and> (b \<noteq> NullCap \<longrightarrow> is_final_cap' rv s) \<or> is_zombie a \<and> is_final_cap' rv s \<and> is_final_cap' a s \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None\<rbrakk> \<Longrightarrow> (cap_removeable a slot \<longrightarrow> Q s) \<and> (\<not> cap_removeable a slot \<longrightarrow> (cap_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> Q s) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> Q s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a a b s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> a; P s; replaceable s slot a rv; emptyable slot s; \<forall>t\<in>obj_refs_ac a. halted_if_tcb t s; ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s; a = NullCap \<and> b = (if rva then cap_cleanup_opt rv else NullCap) \<and> (b \<noteq> NullCap \<longrightarrow> is_final_cap' rv s) \<or> is_zombie a \<and> is_final_cap' rv s \<and> is_final_cap' a s \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None; valid_global_objs s\<rbrakk> \<Longrightarrow> (cap_removeable a slot \<longrightarrow> Q s) \<and> (\<not> cap_removeable a slot \<longrightarrow> (cap_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> Q s) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> Q s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a a b s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> a; P s; replaceable s slot a rv; emptyable slot s; \<forall>t\<in>obj_refs_ac a. halted_if_tcb t s; ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s; a = NullCap \<and> b = (if rva then cap_cleanup_opt rv else NullCap) \<and> (b \<noteq> NullCap \<longrightarrow> is_final_cap' rv s) \<or> is_zombie a \<and> is_final_cap' rv s \<and> is_final_cap' a s \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None; valid_global_objs s; Q s\<rbrakk> \<Longrightarrow> (cap_removeable a slot \<longrightarrow> Q s) \<and> (\<not> cap_removeable a slot \<longrightarrow> (cap_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> Q s) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> Q s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a a b s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> a; P s; replaceable s slot a rv; emptyable slot s; \<forall>t\<in>obj_refs_ac a. halted_if_tcb t s; ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s; valid_global_objs s; Q s; a = NullCap \<and> b = (if rva then cap_cleanup_opt rv else NullCap) \<and> (b \<noteq> NullCap \<longrightarrow> is_final_cap' rv s)\<rbrakk> \<Longrightarrow> (cap_removeable a slot \<longrightarrow> Q s) \<and> (\<not> cap_removeable a slot \<longrightarrow> (cap_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> Q s) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> Q s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a))
 2. \<And>rv s'' rva s''a a b s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> a; P s; replaceable s slot a rv; emptyable slot s; \<forall>t\<in>obj_refs_ac a. halted_if_tcb t s; ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s; valid_global_objs s; Q s; is_zombie a \<and> is_final_cap' rv s \<and> is_final_cap' a s \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None\<rbrakk> \<Longrightarrow> (cap_removeable a slot \<longrightarrow> Q s) \<and> (\<not> cap_removeable a slot \<longrightarrow> (cap_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> Q s) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> Q s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 5. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a a b s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> a; P s; replaceable s slot a rv; emptyable slot s; \<forall>t\<in>obj_refs_ac a. halted_if_tcb t s; ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s; valid_global_objs s; Q s; is_zombie a \<and> is_final_cap' rv s \<and> is_final_cap' a s \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None\<rbrakk> \<Longrightarrow> (cap_removeable a slot \<longrightarrow> Q s) \<and> (\<not> cap_removeable a slot \<longrightarrow> (cap_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> Q s) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a \<and> (\<not> exposed \<longrightarrow> (slot \<in> cte_refs rv (interrupt_irq_node s) \<and> cap_irqs rv = {} \<longrightarrow> slot \<in> cte_refs a (interrupt_irq_node s) \<and> cap_irqs a = {}) \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs a. halted_if_tcb x s) \<and> a \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap a) slot s \<and> Q s \<and> is_final_cap' a s \<and> (obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> cap_irqs a \<inter> cap_irqs rv \<noteq> {}) \<and> is_zombie a))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a s r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> Zombie r b n; P s; replaceable s slot (Zombie r b n) rv; emptyable slot s; halted_if_tcb r s; ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s; valid_global_objs s; Q s; is_final_cap' rv s; is_final_cap' (Zombie r b n) s; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap rv; cte_refs (Zombie r b n) = cte_refs rv; {r} = obj_refs rv; {} = cap_irqs rv; {} = arch_gen_refs rv; (case b of None \<Rightarrow> 0x200 | Some n \<Rightarrow> 2 ^ (cte_level_bits + n)) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; cap_cyclic_zombie (Zombie r b n) slot \<longrightarrow> exposed; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot\<rbrakk> \<Longrightarrow> obj_refs rv \<noteq> {} \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {} \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {} \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {}
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a s r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> Zombie r b n; P s; replaceable s slot (Zombie r b n) rv; emptyable slot s; halted_if_tcb r s; ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s; valid_global_objs s; Q s; is_final_cap' rv s; is_final_cap' (Zombie r b n) s; cte_refs (Zombie r b n) = cte_refs rv; {r} = obj_refs rv; {} = cap_irqs rv; {} = arch_gen_refs rv; (case b of None \<Rightarrow> 0x200 | Some n \<Rightarrow> 2 ^ (cte_level_bits + n)) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; cap_cyclic_zombie (Zombie r b n) slot \<longrightarrow> exposed; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot; appropriate_cte_cap rv = (\<lambda>cap. cap_irqs cap = {})\<rbrakk> \<Longrightarrow> obj_refs rv \<noteq> {} \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {} \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {} \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {}
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a s r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> Zombie r b n; P s; replaceable s slot (Zombie r b n) rv; emptyable slot s; halted_if_tcb r s; ex_cte_cap_wp_to (\<lambda>cap. cap_irqs cap = {}) slot s; valid_global_objs s; Q s; is_final_cap' rv s; is_final_cap' (Zombie r b n) s; cte_refs (Zombie r b n) = cte_refs rv; {r} = obj_refs rv; {} = cap_irqs rv; {} = arch_gen_refs rv; (case b of None \<Rightarrow> 0x200 | Some n \<Rightarrow> 2 ^ (cte_level_bits + n)) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; cap_cyclic_zombie (Zombie r b n) slot \<longrightarrow> exposed; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot; appropriate_cte_cap rv = (\<lambda>cap. cap_irqs cap = {})\<rbrakk> \<Longrightarrow> obj_refs rv \<noteq> {} \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {} \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {} \<and> (\<forall>x\<in>obj_refs rv. halted_if_tcb x s) \<and> obj_refs rv \<noteq> {}
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a s r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); invs s; caps_of_state s slot = Some rv; s \<turnstile> Zombie r b n; P s; replaceable s slot (Zombie r b n) rv; emptyable slot s; halted_if_tcb r s; ex_cte_cap_wp_to (\<lambda>cap. cap_irqs cap = {}) slot s; valid_global_objs s; Q s; is_final_cap' rv s; is_final_cap' (Zombie r b n) s; cte_refs (Zombie r b n) = cte_refs rv; {} = cap_irqs rv; {} = arch_gen_refs rv; (case b of None \<Rightarrow> 0x200 | Some n \<Rightarrow> 2 ^ (cte_level_bits + n)) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; cap_cyclic_zombie (Zombie r b n) slot \<longrightarrow> exposed; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot; appropriate_cte_cap rv = (\<lambda>cap. cap_irqs cap = {})\<rbrakk> \<Longrightarrow> {r} \<noteq> {} \<and> (\<forall>x\<in>{r}. halted_if_tcb x s) \<and> {r} \<noteq> {} \<and> (\<forall>x\<in>{r}. halted_if_tcb x s) \<and> {r} \<noteq> {} \<and> (\<forall>x\<in>{r}. halted_if_tcb x s) \<and> {r} \<noteq> {}
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((invs and cte_wp_at ((=) rv) slot) s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> (R rv and P) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> (emptyable slot and invs) s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> liftE (gets (is_final_cap' rv)) \<lbrace>\<lambda>rva s. invs s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> R rv s \<and> P s \<and> s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s) \<and> emptyable slot s \<and> invs s \<and> s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s \<and> Q s) \<and> (rv \<noteq> NullCap \<longrightarrow> invs s \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> rv \<and> R rv s \<and> P s \<and> s \<turnstile> rv \<and> is_final_cap' rv s = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s) \<and> emptyable slot s \<and> invs s \<and> s \<turnstile> rv \<and> is_final_cap' rv s = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and> (is_final_cap' rv s \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s))\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap = NullCap \<longrightarrow> P s \<and> Q s) \<and> (cap \<noteq> NullCap \<longrightarrow> invs s \<and> cte_wp_at ((=) cap) slot s \<and> s \<turnstile> cap \<and> R cap s \<and> P s \<and> s \<turnstile> cap \<and> is_final_cap' cap s = is_final_cap' cap s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s) \<and> emptyable slot s \<and> invs s \<and> s \<turnstile> cap \<and> is_final_cap' cap s = is_final_cap' cap s \<and> cte_wp_at ((=) cap) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s \<and> (is_final_cap' cap s \<longrightarrow> is_final_cap' cap s \<and> cte_wp_at ((=) cap) slot s)) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; P s; Q s; emptyable slot s; caps_of_state s slot = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> s \<turnstile> cap \<and> R cap s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> valid_arch_caps s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; P s; Q s; emptyable slot s; caps_of_state s slot = Some cap; cap \<noteq> NullCap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> s \<turnstile> cap \<and> R cap s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> valid_arch_caps s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>P s; Q s; emptyable slot s; caps_of_state s slot = Some cap; cap \<noteq> NullCap; s \<turnstile> cap; equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) s \<and> valid_rec_del_call (FinaliseSlotCall slot exposed) s\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>

goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = s \<and> invs s \<and> P s \<and> Q s \<and> emptyable slot s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n))\<rbrace> doE y <- assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot);
y <- liftE (cap_swap_for_delete (ptr, replicate (zombie_cte_bits bits) False) slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s = s \<and> invs s \<and> P s \<and> Q s \<and> emptyable slot s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n)) \<Longrightarrow> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> (Q and P) s \<and> Q s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (state)
this:
(Inr ?rv, ?st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ?st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall ?rv False)) s \<and> valid_rec_del_call (CTEDeleteCall ?rv False) s\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> doE end_slot <- returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n);
rec_del (CTEDeleteCall end_slot False);
new_cap <- without_preemption $ get_cap slot;
if new_cap = Zombie ptr bits (Suc n) then without_preemption $ set_cap (Zombie ptr bits n) slot else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> doE end_slot <- returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n);
rec_del (CTEDeleteCall end_slot False);
new_cap <- without_preemption $ get_cap slot;
if new_cap = Zombie ptr bits (Suc n) then without_preemption $ set_cap (Zombie ptr bits n) slot else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B3 rv\<rbrace> doE rec_del (CTEDeleteCall rv False);
new_cap <- without_preemption $ get_cap slot;
if new_cap = Zombie ptr bits (Suc n) then without_preemption $ set_cap (Zombie ptr bits n) slot else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. s \<turnstile> \<lbrace>?P'\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B3 rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?B6 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B6 rv s'' rva\<rbrace> K_bind (doE new_cap <- without_preemption $ get_cap slot;
if new_cap = Zombie ptr bits (Suc n) then without_preemption $ set_cap (Zombie ptr bits n) slot else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot);
returnOk undefined
odE) rva \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 4. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>\<lambda>s. P s \<and> Q s\<rbrace> K_bind (doE new_cap <- without_preemption $ get_cap slot;
if new_cap = Zombie ptr bits (Suc n) then without_preemption $ set_cap (Zombie ptr bits n) slot else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot);
returnOk undefined
odE) rva \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. s \<turnstile> \<lbrace>?P'\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a s. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s''); P s \<and> Q s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (Q and P) s \<and> Q s) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> cap = NullCap \<or> is_zombie cap \<and> first_cslot_of cap = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot \<longrightarrow> P s \<and> Q s)
 2. s \<turnstile> \<lbrace>?P'\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 3. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (CTEDeleteCall rv False)) s \<and> valid_rec_del_call (CTEDeleteCall rv False) s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. invs s \<and> P s \<and> Q s \<and> emptyable rv s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s \<Longrightarrow> invs s \<and> P s \<and> Q s \<and> emptyable (ptr, nat_to_cref (zombie_cte_bits bits) n) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; P s; Q s; emptyable slot s; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s; is_final_cap' (Zombie ptr bits (Suc n)) s; is_zombie (Zombie ptr bits (Suc n))\<rbrakk> \<Longrightarrow> emptyable (ptr, nat_to_cref (zombie_cte_bits bits) n) s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s \<and> valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>

goal:
No subgoals!