theory Tcb_AI

lemma (in Tcb_AI_1) rec_del_all_caps_in_range:
  assumes x: "P cap.NullCap"
      and y: "\<And>x n zt. P (cap.ThreadCap x) \<Longrightarrow> P (cap.Zombie x zt n)"
      and z: "\<And>x y gd n zt. P (cap.CNodeCap x y gd) \<Longrightarrow> P (cap.Zombie x zt n)"
      and w: "\<And>x zt zt' n m. P (cap.Zombie x zt n) \<Longrightarrow> P (cap.Zombie x zt' m)"
  shows      "s \<turnstile> \<lbrace>\<lambda>(s::'state_ext state). \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>
                     rec_del args
                  \<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>,
                  \<lbrace>\<lambda>e s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>" proof (induct rule: rec_del.induct, simp_all only: rec_del_fails) case (1 slot exposed s') note hyps = "1.hyps"[simplified slot_rdcall.simps rec_del_call.simps simp_thms] show ?case apply (simp add: split_def) apply wp apply (wp empty_slot_caps_of_state)[1] apply (rule spec_strengthen_postE, rule hyps) apply (clarsimp simp add: x ball_ran_eq) done next case (2 slot exposed s') note hyps = "2.hyps"[simplified slot_rdcall.simps rec_del_call.simps simp_thms] show ?case apply (simp add: split_def cong: if_cong) apply (wp hyps, simp+) apply ((wp irq_state_independent_AI preemption_point_inv | simp)+)[1] apply (simp only: simp_thms) apply (wp hyps, simp+) apply wp+ apply (rule hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule finalise_cap_cases[where slot=slot]) apply (rule hoare_vcg_conj_lift) apply (rule finalise_cap_equal_cap[where sl=slot]) apply (rule finalise_cap_not_cte_wp_at[where P=P, OF x]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule disjE) apply clarsimp apply (clarsimp simp: is_cap_simps ball_ran_eq) apply (subgoal_tac "P rv") apply (case_tac rv, simp_all add: fst_cte_ptrs_def gen_obj_refs_eq)[1] apply (simp add: z) apply (simp add: y) apply (simp split: option.split_asm, simp_all add: w gen_obj_refs_eq)[1] apply (cases slot, fastforce) apply (simp add: is_final_cap_def) apply (wp get_cap_wp)+ apply clarsimp done next case (3 ptr bits n slot s') show ?case apply simp apply wp+ apply (cases slot) apply (clarsimp del: ballI simp: ball_ran_eq) done next case (4 ptr bits n slot s') show ?case apply simp apply wp apply (wp get_cap_wp)[1] apply (rule spec_strengthen_postE, rule "4.hyps") apply (simp add: in_monad) apply (clarsimp del: ballI simp: ball_ran_eq) apply (fastforce simp: cte_wp_at_caps_of_state
                    elim: w) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del args \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (state)
goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (state)
this:
s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (state)
this:
s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> doE p <- rec_del (FinaliseSlotCall slot exposed);
y <- liftE (when (exposed \<or> fst p) (empty_slot slot (snd p)));
returnOk undefined
odE \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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>?Q9 rv\<rbrace> empty_slot slot (snd rv) \<lbrace>\<lambda>a b. \<forall>cp\<in>ran (caps_of_state b). P cp\<rbrace>
 2. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then ?Q9 a else (\<lambda>a. \<forall>cp\<in>ran (caps_of_state a). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then \<lambda>a. \<forall>cp\<in>ran ((caps_of_state a)(slot \<mapsto> NullCap)). P cp else (\<lambda>a. \<forall>cp\<in>ran (caps_of_state a). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<forall>cp\<in>ran (caps_of_state r). P cp \<Longrightarrow> (if exposed \<or> fst s then \<lambda>a. \<forall>cp\<in>ran ((caps_of_state a)(slot \<mapsto> NullCap)). P cp else (\<lambda>a. \<forall>cp\<in>ran (caps_of_state a). P cp)) r proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> doE cap <- liftE (get_cap slot);
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- liftE (is_final_cap cap);
p <- liftE (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 y <- liftE (set_cap (fst p) slot);
returnOk (False, NullCap)
odE else doE y <- liftE (set_cap (fst p) slot);
y <- rec_del (ReduceZombieCall (fst p) slot exposed);
y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s'); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (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>?B41 rv s'' rva s''a rvb s''b () s''c rvd\<rbrace> preemption_point \<lbrace>\<lambda>rve s. \<forall>x\<in>ran (caps_of_state s). P x\<rbrace>, \<lbrace>\<lambda>e s. \<forall>x\<in>ran (caps_of_state s). P x\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst (liftE (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 (liftE (set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B40 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B41 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst (liftE (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'29 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B40 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'29 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 6. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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 (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst (liftE (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 (liftE (set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B40 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a b. (\<forall>x\<in>ran (caps_of_state b). P x) \<and> (\<forall>x\<in>ran (caps_of_state b). P x)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst (liftE (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'29 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B40 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'29 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 5. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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 (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst (liftE (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 (liftE (set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B40 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a b. Ball (ran (caps_of_state b)) P\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst (liftE (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'29 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B40 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'29 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 5. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s'); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'29 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>\<lambda>rvc s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'29 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B16 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)))\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B16 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q77 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); ?Q77 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P81 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q80 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'82 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q'80 rv s'' rva s''a\<rbrace>
 3. \<And>rv s'' rva s''a rvb s. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); ?Q80 rv s'' rva s''a rvb s \<and> ?Q'80 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)))
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. ?P81 rv s'' rva s \<and> ?P'82 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 5. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'82 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q'80 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (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) \<and> ?Q'80 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> ?P'82 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P90 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q89 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'91 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q'89 rv s'' rva s''a\<rbrace>
 3. \<And>rv s'' rva s''a rvb s. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (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) \<and> ?Q89 rv s'' rva s''a rvb s \<and> ?Q'89 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)))
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> ?P90 rv s'' rva s \<and> ?P'91 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 5. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'91 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q'89 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (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) \<and> cte_wp_at ((=) rv) slot s \<and> ?Q'89 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> ?P'91 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a rvb s. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (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) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> fst rvb)). P cp)))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (3 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''); 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; caps_of_state s slot = Some rv; \<forall>x\<in>ran (caps_of_state s). P x; \<not> cap_removeable a slot\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> (\<forall>x\<in>ran (\<lambda>b. if b = slot then Some a else caps_of_state s b). P x)) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> (\<forall>x\<in>ran (\<lambda>b. if b = slot then Some a else caps_of_state s b). P x))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> 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''); caps_of_state s slot = Some rv; \<forall>x\<in>ran (caps_of_state s). P x; \<not> cap_removeable a slot; 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_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> (\<forall>x\<in>ran (\<lambda>b. if b = slot then Some a else caps_of_state s b). P x)) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> (\<forall>x\<in>ran (\<lambda>b. if b = slot then Some a else caps_of_state s b). P x))
 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''); caps_of_state s slot = Some rv; \<forall>x\<in>ran (caps_of_state s). P x; \<not> cap_removeable a slot; 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_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> (\<forall>x\<in>ran (\<lambda>b. if b = slot then Some a else caps_of_state s b). P x)) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> (\<forall>x\<in>ran (\<lambda>b. if b = slot then Some a else caps_of_state s b). P x))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (3 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''); caps_of_state s slot = Some rv; \<forall>x\<in>ran (caps_of_state s). P x; \<not> cap_removeable a slot; 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_cyclic_zombie a slot \<and> \<not> exposed \<longrightarrow> (\<forall>x\<in>ran (\<lambda>b. if b = slot then Some a else caps_of_state s b). P x)) \<and> ((cap_cyclic_zombie a slot \<longrightarrow> exposed) \<longrightarrow> (\<forall>x\<in>ran (\<lambda>b. if b = slot then Some a else caps_of_state s b). P x))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (3 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''); caps_of_state s slot = Some rv; \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; 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; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) slot \<and> \<not> exposed \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie r b n)) \<and> ((cap_cyclic_zombie (Zombie r b n) slot \<longrightarrow> exposed) \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie r b n))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> 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''); caps_of_state s slot = Some rv; \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; 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; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot; P rv\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) slot \<and> \<not> exposed \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie r b n)) \<and> ((cap_cyclic_zombie (Zombie r b n) slot \<longrightarrow> exposed) \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie r b n))
 2. \<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''); caps_of_state s slot = Some rv; \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; 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; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot\<rbrakk> \<Longrightarrow> P rv
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a s r b n x61 x62 x63. \<lbrakk>(CNodeCap x61 x62 x63, s'') \<in> fst (get_cap slot s'); (rva, s''a) \<in> fst (is_final_cap (CNodeCap x61 x62 x63) s''); caps_of_state s slot = Some (CNodeCap x61 x62 x63); \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; is_final_cap' (CNodeCap x61 x62 x63) s; is_final_cap' (Zombie x61 b n) s; appropriate_cte_cap (Zombie x61 b n) = appropriate_cte_cap (CNodeCap x61 x62 x63); cte_refs (Zombie x61 b n) = cte_refs (CNodeCap x61 x62 x63); r = x61; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = 2 ^ (cte_level_bits + x62); zombie_cte_bits b = x62; vs_cap_ref (CNodeCap x61 x62 x63) = None; 0 < n; n = Suc 0 \<longrightarrow> (x61, replicate x62 False) \<noteq> slot; P (CNodeCap x61 x62 x63); rv = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie x61 b n) slot \<and> \<not> exposed \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x61 b n)) \<and> ((cap_cyclic_zombie (Zombie x61 b n) slot \<longrightarrow> exposed) \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x61 b n))
 2. \<And>rv s'' rva s''a s r b n x7. \<lbrakk>(ThreadCap x7, s'') \<in> fst (get_cap slot s'); (rva, s''a) \<in> fst (is_final_cap (ThreadCap x7) s''); caps_of_state s slot = Some (ThreadCap x7); \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; is_final_cap' (ThreadCap x7) s; is_final_cap' (Zombie x7 b n) s; appropriate_cte_cap (Zombie x7 b n) = appropriate_cte_cap (ThreadCap x7); cte_refs (Zombie x7 b n) = cte_refs (ThreadCap x7); r = x7; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = 0x200; replicate (zombie_cte_bits b) False = tcb_cnode_index 0; vs_cap_ref (ThreadCap x7) = None; 0 < n; n = Suc 0 \<longrightarrow> (x7, tcb_cnode_index 0) \<noteq> slot; P (ThreadCap x7); rv = ThreadCap x7\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie x7 b n) slot \<and> \<not> exposed \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x7 b n)) \<and> ((cap_cyclic_zombie (Zombie x7 b n) slot \<longrightarrow> exposed) \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x7 b n))
 3. \<And>rv s'' rva s''a s r b n x111 x112 x113. \<lbrakk>(Zombie x111 x112 x113, s'') \<in> fst (get_cap slot s'); (rva, s''a) \<in> fst (is_final_cap (Zombie x111 x112 x113) s''); caps_of_state s slot = Some (Zombie x111 x112 x113); \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; is_final_cap' (Zombie x111 x112 x113) s; is_final_cap' (Zombie x111 b n) s; appropriate_cte_cap (Zombie x111 b n) = appropriate_cte_cap (Zombie x111 x112 x113); cte_refs (Zombie x111 b n) = cte_refs (Zombie x111 x112 x113); r = x111; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = (case x112 of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n); zombie_cte_bits b = zombie_cte_bits x112; vs_cap_ref (Zombie x111 x112 x113) = None; 0 < n; n = Suc 0 \<longrightarrow> (x111, replicate (zombie_cte_bits x112) False) \<noteq> slot; P (Zombie x111 x112 x113); rv = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie x111 b n) slot \<and> \<not> exposed \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x111 b n)) \<and> ((cap_cyclic_zombie (Zombie x111 b n) slot \<longrightarrow> exposed) \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x111 b n))
 4. \<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''); caps_of_state s slot = Some rv; \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; 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; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot\<rbrakk> \<Longrightarrow> P rv
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 6. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a s r b n x7. \<lbrakk>(ThreadCap x7, s'') \<in> fst (get_cap slot s'); (rva, s''a) \<in> fst (is_final_cap (ThreadCap x7) s''); caps_of_state s slot = Some (ThreadCap x7); \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; is_final_cap' (ThreadCap x7) s; is_final_cap' (Zombie x7 b n) s; appropriate_cte_cap (Zombie x7 b n) = appropriate_cte_cap (ThreadCap x7); cte_refs (Zombie x7 b n) = cte_refs (ThreadCap x7); r = x7; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = 0x200; replicate (zombie_cte_bits b) False = tcb_cnode_index 0; vs_cap_ref (ThreadCap x7) = None; 0 < n; n = Suc 0 \<longrightarrow> (x7, tcb_cnode_index 0) \<noteq> slot; P (ThreadCap x7); rv = ThreadCap x7\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie x7 b n) slot \<and> \<not> exposed \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x7 b n)) \<and> ((cap_cyclic_zombie (Zombie x7 b n) slot \<longrightarrow> exposed) \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x7 b n))
 2. \<And>rv s'' rva s''a s r b n x111 x112 x113. \<lbrakk>(Zombie x111 x112 x113, s'') \<in> fst (get_cap slot s'); (rva, s''a) \<in> fst (is_final_cap (Zombie x111 x112 x113) s''); caps_of_state s slot = Some (Zombie x111 x112 x113); \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; is_final_cap' (Zombie x111 x112 x113) s; is_final_cap' (Zombie x111 b n) s; appropriate_cte_cap (Zombie x111 b n) = appropriate_cte_cap (Zombie x111 x112 x113); cte_refs (Zombie x111 b n) = cte_refs (Zombie x111 x112 x113); r = x111; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = (case x112 of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n); zombie_cte_bits b = zombie_cte_bits x112; vs_cap_ref (Zombie x111 x112 x113) = None; 0 < n; n = Suc 0 \<longrightarrow> (x111, replicate (zombie_cte_bits x112) False) \<noteq> slot; P (Zombie x111 x112 x113); rv = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie x111 b n) slot \<and> \<not> exposed \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x111 b n)) \<and> ((cap_cyclic_zombie (Zombie x111 b n) slot \<longrightarrow> exposed) \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x111 b n))
 3. \<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''); caps_of_state s slot = Some rv; \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; 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; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot\<rbrakk> \<Longrightarrow> P rv
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 5. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a s r b n x111 x112 x113. \<lbrakk>(Zombie x111 x112 x113, s'') \<in> fst (get_cap slot s'); (rva, s''a) \<in> fst (is_final_cap (Zombie x111 x112 x113) s''); caps_of_state s slot = Some (Zombie x111 x112 x113); \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; is_final_cap' (Zombie x111 x112 x113) s; is_final_cap' (Zombie x111 b n) s; appropriate_cte_cap (Zombie x111 b n) = appropriate_cte_cap (Zombie x111 x112 x113); cte_refs (Zombie x111 b n) = cte_refs (Zombie x111 x112 x113); r = x111; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = (case x112 of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n); zombie_cte_bits b = zombie_cte_bits x112; vs_cap_ref (Zombie x111 x112 x113) = None; 0 < n; n = Suc 0 \<longrightarrow> (x111, replicate (zombie_cte_bits x112) False) \<noteq> slot; P (Zombie x111 x112 x113); rv = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie x111 b n) slot \<and> \<not> exposed \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x111 b n)) \<and> ((cap_cyclic_zombie (Zombie x111 b n) slot \<longrightarrow> exposed) \<longrightarrow> (\<exists>a b. (a, b) = slot) \<longrightarrow> P (Zombie x111 b n))
 2. \<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''); caps_of_state s slot = Some rv; \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; 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; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot\<rbrakk> \<Longrightarrow> P rv
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 4. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (3 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''); caps_of_state s slot = Some rv; \<forall>a b y. caps_of_state s (a, b) = Some y \<longrightarrow> P y; 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; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot\<rbrakk> \<Longrightarrow> P rv
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 3. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s'); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'13 rv\<rbrace> liftE (gets (is_final_cap' rv)) \<lbrace>\<lambda>rva s. (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s) \<and> cte_wp_at ((=) rv) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>
 2. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'13 rv s)\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>cp\<in>ran (caps_of_state s). P cp \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap = NullCap \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp)) \<and> (cap \<noteq> NullCap \<longrightarrow> (is_final_cap' cap s \<longrightarrow> is_final_cap' cap s \<and> cte_wp_at ((=) cap) slot s) \<and> cte_wp_at ((=) cap) slot s \<and> (\<forall>cp\<in>ran (caps_of_state s). P cp)) proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>

goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>cp\<in>ran (caps_of_state s). P cp \<Longrightarrow> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s \<circ> id((ptr, replicate (zombie_cte_bits bits) False) := slot, slot := (ptr, replicate (zombie_cte_bits bits) False))). P cp) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>cp\<in>ran (caps_of_state s). P cp; slot = (a, b)\<rbrakk> \<Longrightarrow> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s \<circ> id((ptr, replicate (zombie_cte_bits bits) False) := slot, slot := (ptr, replicate (zombie_cte_bits bits) False))). P cp) proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<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. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> doE y <- rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False);
new_cap <- liftE (get_cap slot);
y <- if new_cap = Zombie ptr bits (Suc n) then liftE (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> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) s') \<Longrightarrow> \<lbrace>?B4 rv\<rbrace> get_cap slot \<lbrace>\<lambda>rva s. (rva = Zombie ptr bits (Suc n) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> Zombie ptr bits n)). P cp)) \<and> (rva \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> rva = NullCap \<or> is_zombie rva \<and> first_cslot_of rva = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp))\<rbrace>
 2. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>rv s. \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state s)(slot \<mapsto> Zombie ptr bits n)). P cp)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> cap = NullCap \<or> is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state s). P cp))\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> proof (prove)
goal (2 subgoals):
 1. (Inr (ptr, nat_to_cref (zombie_cte_bits bits) n), s') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s')
 2. \<And>s r. \<forall>cp\<in>ran (caps_of_state r). P cp \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state r)(slot \<mapsto> Zombie ptr bits n)). P cp)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> cap = NullCap \<or> is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state r). P cp)) proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<forall>cp\<in>ran (caps_of_state r). P cp \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<forall>cp\<in>ran ((caps_of_state r)(slot \<mapsto> Zombie ptr bits n)). P cp)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> cap = NullCap \<or> is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> (\<forall>cp\<in>ran (caps_of_state r). P cp)) proof (prove)
goal (1 subgoal):
 1. \<And>r a b. \<lbrakk>\<forall>a b y. caps_of_state r (a, b) = Some y \<longrightarrow> P y; cte_wp_at ((=) (Zombie ptr bits (Suc n))) (a, b) r; slot = (a, b)\<rbrakk> \<Longrightarrow> P (Zombie ptr bits n) proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>, \<lbrace>\<lambda>e s. \<forall>cp\<in>ran (caps_of_state s). P cp\<rbrace>

goal:
No subgoals!