theory CNodeInv_AI

lemma rec_del_preservation':
  fixes s :: "'state_ext state"
  fixes P :: "'state_ext state \<Rightarrow> bool"
  assumes wp:
    "\<And>sl1 sl2. \<lbrace>P\<rbrace> cap_swap_for_delete sl1 sl2 \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>sl cap. \<lbrace>P\<rbrace> set_cap sl cap \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>sl opt. \<lbrace>P\<rbrace> empty_slot sl opt \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>cap fin. \<lbrace>P\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<lbrace>P\<rbrace> preemption_point \<lbrace>\<lambda>rv. P\<rbrace>"
  shows
  "s \<turnstile> \<lbrace>P\<rbrace> rec_del call \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>" proof (induct rule: rec_del_induct) case (1 slot exposed s) show ?case apply (subst rec_del_simps) apply (simp only: split_def) apply wp apply (wp wp)[1] apply (rule spec_strengthen_postE) apply (rule "1.hyps") apply simp done next case (2 slot exposed s) show ?case apply (subst rec_del_simps) apply (simp only: split_def) apply (wp wp "2.hyps") apply (wp wp)[1] apply (simp only: simp_thms) apply (rule "2.hyps", assumption+) apply (wp wp hoare_drop_imps | simp add: is_final_cap_def)+ done next case 3 show ?case apply (simp add: rec_del_simps | wp wp)+ done next case (4 ptr bits n slot s) show ?case apply (subst rec_del_simps) apply (wp wp) apply (wp hoare_drop_imps)[1] apply (simp only: simp_thms) apply (rule "4.hyps", assumption+) apply wp done qed (auto simp: rec_del_dom rec_del_fails)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> rec_del call \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (state)
goal (28 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (CTEDeleteCall slot exposed, s); s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>rec_del_dom (FinaliseSlotCall slot exposed, s); \<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>P\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<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>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 28 subgoals... proof (state)
this:
rec_del_dom (CTEDeleteCall slot exposed, s)
s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>

goal (28 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (CTEDeleteCall slot exposed, s); s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>rec_del_dom (FinaliseSlotCall slot exposed, s); \<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>P\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<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>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 28 subgoals... proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<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>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 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>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (rec_del (FinaliseSlotCall slot exposed) s); exposed \<or> fst rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> empty_slot slot (snd rv) \<lbrace>\<lambda>a. P\<rbrace>
 2. s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then ?Q12 a else P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then P else P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>?Q'16\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s r. ?Q'16 s r \<Longrightarrow> (if exposed \<or> fst s then P else P) r proof (prove)
goal (1 subgoal):
 1. \<And>s r. P r \<Longrightarrow> (if exposed \<or> fst s then P else P) r proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>

goal (27 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (FinaliseSlotCall slot exposed, s); \<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>P\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<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>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 27 subgoals... proof (state)
goal (27 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (FinaliseSlotCall slot exposed, s); \<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>P\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<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>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 27 subgoals... proof (state)
this:
rec_del_dom (FinaliseSlotCall slot exposed, s)
\<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>P\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<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>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>

goal (27 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (FinaliseSlotCall slot exposed, s); \<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>P\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<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>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 27 subgoals... proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 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;
(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>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 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>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (6 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> s''d \<turnstile> \<lbrace>?B32 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>\<lambda>rve. P\<rbrace>, \<lbrace>\<lambda>_. P\<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>?B30 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B32 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. P\<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'21 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B30 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. P\<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>?B8 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> P s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'21 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. P\<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'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B8 rv s''\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. s \<turnstile> \<lbrace>P\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (5 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>?B30 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>_. P\<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'21 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B30 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. P\<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>?B8 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> P s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'21 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. P\<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'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B8 rv s''\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. s \<turnstile> \<lbrace>P\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (5 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>?B30 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd. P\<rbrace>, \<lbrace>\<lambda>_. P\<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'21 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B30 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. P\<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>?B8 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> P s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'21 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. P\<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'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B8 rv s''\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. s \<turnstile> \<lbrace>P\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (4 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; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'21 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>rvc. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<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>?B8 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> P s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> P s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'21 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 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'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B8 rv s''\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. s \<turnstile> \<lbrace>P\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> P s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>

goal (26 subgoals):
 1. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>slot exposed s. rec_del_dom (ReduceZombieCall DomainCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall DomainCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 26 subgoals... proof (state)
goal (26 subgoals):
 1. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>slot exposed s. rec_del_dom (ReduceZombieCall DomainCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall DomainCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 26 subgoals... proof (state)
this:
rec_del_dom (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False, s_)

goal (26 subgoals):
 1. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>slot exposed s. rec_del_dom (ReduceZombieCall DomainCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall DomainCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 26 subgoals... proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
s_ \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>

goal (25 subgoals):
 1. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>slot exposed s. rec_del_dom (ReduceZombieCall DomainCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall DomainCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>slot exposed s. rec_del_dom (ReduceZombieCall IRQControlCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall IRQControlCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 25 subgoals... proof (state)
goal (25 subgoals):
 1. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>slot exposed s. rec_del_dom (ReduceZombieCall DomainCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall DomainCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>slot exposed s. rec_del_dom (ReduceZombieCall IRQControlCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall IRQControlCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 25 subgoals... proof (state)
this:
rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s)
(Inr ?rv, ?st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ?st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>

goal (25 subgoals):
 1. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>P\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>slot exposed s. rec_del_dom (ReduceZombieCall DomainCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall DomainCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>slot exposed s. rec_del_dom (ReduceZombieCall IRQControlCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall IRQControlCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 25 subgoals... proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 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>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> 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> \<lbrace>?B1 rv s'' rva\<rbrace> get_cap slot \<lbrace>\<lambda>rvb s. (rvb = Zombie ptr bits (Suc n) \<longrightarrow> P s) \<and> (rvb \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> rvb = NullCap \<or> is_zombie rvb \<and> first_cslot_of rvb = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot \<longrightarrow> P s)\<rbrace>
 2. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?B1 rv s''\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. s \<turnstile> \<lbrace>P\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 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>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. s \<turnstile> \<lbrace>P\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 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>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. s \<turnstile> \<lbrace>P\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>

goal (24 subgoals):
 1. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall NullCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (UntypedCap v va vb vc) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (EndpointCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (NotificationCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ReplyCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (CNodeCap v va vb) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (ThreadCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 8. \<And>slot exposed s. rec_del_dom (ReduceZombieCall DomainCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall DomainCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>slot exposed s. rec_del_dom (ReduceZombieCall IRQControlCap slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall IRQControlCap slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (IRQHandlerCap v) slot exposed, s) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> rec_del (ReduceZombieCall (IRQHandlerCap v) slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
A total of 24 subgoals...