theory CNodeInv_AI

lemma rec_del_termination:
  "All (rec_del_dom :: rec_del_call \<times> 'state_ext state \<Rightarrow> bool)"
  \<comment> \<open> rec_del.termination needs a well-formed measure and proofs that the 4 recursive calls
       reduce this measure. \<close> apply (rule rec_del.termination[where R=rec_del_recset])

      \<comment> \<open> The measure is well-formed. \<close> apply (rule rec_del_recset_wf)

     \<comment> \<open> case 1: CTEDeleteCall --> FinaliseSlotCall \<close> apply (simp add: rec_del_recset_def wf_sum_def rdcall_finalise_ord_lift_def mlex_prod_def)

    \<comment> \<open> case 2: FinaliseSlotCall --> ReduceZombieCall \<close> apply (simp add: rec_del_recset_def wf_sum_def rdcall_finalise_ord_lift_def mlex_prod_def)

   \<comment> \<open> case 3: FinaliseSlotCall --> FinaliseSlotCall \<close> apply (case_tac exposed; simp)

    \<comment> \<open> FinaliseSlotCall _ True --> FinaliseSlotCall _ True \<close> apply (simp add: rec_del_recset_def wf_sum_def rdcall_finalise_ord_lift_def mlex_prod_def) apply (rule disjI1, rule map_prod_split_imageI, clarsimp) apply (rename_tac oref cref exposed st1 fcap st2 is_final st3 pcap1 pcap2 st4 st5 success
                      cl_info st6 st7) apply (erule use_valid [OF _ preemption_point_caps_of_state]) apply (case_tac pcap1; simp add: fail_def rec_del.psimps) apply (rename_tac word option nat) apply (case_tac nat; simp) apply (clarsimp simp: in_monad rec_del.psimps) apply (clarsimp simp: in_monad in_get_cap_cte_wp_at
                          cte_wp_at_caps_of_state rec_del.psimps
                   split: if_split_asm) apply (erule use_valid [OF _ set_cap_caps_of_state])+ apply (case_tac fcap; clarsimp simp: fst_cte_ptrs_first_cte_of in_monad) apply (case_tac new_cap; simp add: is_cap_simps) apply (case_tac fcap; clarsimp simp: fst_cte_ptrs_first_cte_of) apply (case_tac fcap; clarsimp simp: fst_cte_ptrs_first_cte_of in_monad)

   \<comment> \<open> FinaliseSlotCall _ False --> FinaliseSlotCall _ False \<close> apply (simp add: rec_del_recset_def wf_sum_def rdcall_finalise_ord_lift_def mlex_prod_def) apply (rule disjI2, rule map_prod_split_imageI, clarsimp) apply (rename_tac oref cref exposed st1 fcap st2 is_final st3 pcap1 pcap2 st4 st5 success
                     cl_info st6 st7) apply (simp add: in_monad is_final_cap_def is_zombie_def) apply (erule use_valid [OF _ preemption_point_not_recursive_cspaces]) apply (case_tac pcap1, simp_all add: fail_def rec_del.psimps)[1] apply (rename_tac word option nat) apply (case_tac nat, simp_all) apply (clarsimp simp: in_monad prod_eqI rec_del.psimps) apply (erule use_valid [OF _ cap_swap_fd_not_recursive]) apply (frule use_valid [OF _ get_cap_cte_wp_at, simplified]) apply (drule in_inv_by_hoareD [OF get_cap_inv], clarsimp) apply (erule use_valid [OF _ hoare_vcg_conj_lift [OF set_zombie_not_recursive final_cap_still_at]]) apply (frule use_valid [OF _ finalise_cap_cases]) apply (fastforce simp add: cte_wp_at_eq_simp) apply clarsimp apply (case_tac fcap, simp_all add: fst_cte_ptrs_def) apply (clarsimp simp: in_monad cte_wp_at_caps_of_state fst_cte_ptrs_def
                    split: if_split_asm) apply (clarsimp simp: in_monad cte_wp_at_caps_of_state fst_cte_ptrs_def
                   split: if_split_asm) apply (frule(1) use_valid [OF _ unbind_notification_caps_of_state],
           frule(1) use_valid [OF _ suspend_thread_cap],
           frule(1) use_valid [OF _ prepare_thread_delete_thread_cap]) apply clarsimp apply (erule use_valid [OF _ prepare_thread_delete_not_recursive]) apply (erule use_valid [OF _ suspend_not_recursive]) apply (erule use_valid [OF _ unbind_notification_not_recursive]) apply simp apply (clarsimp simp: in_monad cte_wp_at_caps_of_state
                         fst_cte_ptrs_def zombie_cte_bits_def
                         tcb_cnode_index_def
                  split: option.split_asm)

  \<comment>\<open> case 4: ReduceZombieCall --> CTEDeleteCall \<close> apply (simp add: rec_del_recset_def wf_sum_def rdcall_finalise_ord_lift_def mlex_prod_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. All rec_del_dom proof (prove)
goal (5 subgoals):
 1. wf rec_del_recset
 2. \<And>slot exposed s. ((FinaliseSlotCall slot exposed, s), CTEDeleteCall slot exposed, s) \<in> rec_del_recset
 3. \<And>slot exposed s 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> ((ReduceZombieCall (fst rvb) slot exposed, stc), FinaliseSlotCall slot exposed, s) \<in> rec_del_recset
 4. \<And>slot exposed s 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); rec_del_dom (ReduceZombieCall (fst rvb) slot exposed, stc)\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot exposed, ste), FinaliseSlotCall slot exposed, s) \<in> rec_del_recset
 5. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (4 subgoals):
 1. \<And>slot exposed s. ((FinaliseSlotCall slot exposed, s), CTEDeleteCall slot exposed, s) \<in> rec_del_recset
 2. \<And>slot exposed s 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> ((ReduceZombieCall (fst rvb) slot exposed, stc), FinaliseSlotCall slot exposed, s) \<in> rec_del_recset
 3. \<And>slot exposed s 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); rec_del_dom (ReduceZombieCall (fst rvb) slot exposed, stc)\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot exposed, ste), FinaliseSlotCall slot exposed, s) \<in> rec_del_recset
 4. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>slot exposed s 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> ((ReduceZombieCall (fst rvb) slot exposed, stc), FinaliseSlotCall slot exposed, s) \<in> rec_del_recset
 2. \<And>slot exposed s 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); rec_del_dom (ReduceZombieCall (fst rvb) slot exposed, stc)\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot exposed, ste), FinaliseSlotCall slot exposed, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>slot exposed s 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); rec_del_dom (ReduceZombieCall (fst rvb) slot exposed, stc)\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot exposed, ste), FinaliseSlotCall slot exposed, s) \<in> rec_del_recset
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot True) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot True, stc); exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot True, ste), FinaliseSlotCall slot True, s) \<in> rec_del_recset
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot True) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot True, stc); exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot True, ste), FinaliseSlotCall slot True, s) \<in> map_prod (\<lambda>(x, y). (FinaliseSlotCall x True, y)) (\<lambda>(x, y). (FinaliseSlotCall x True, y)) ` inv_image (less_than <*lex*> less_than) (\<lambda>(x, s). case caps_of_state s x of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {x} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)) \<or> ((FinaliseSlotCall slot True, ste), FinaliseSlotCall slot True, s) \<in> map_prod (\<lambda>(x, y). (FinaliseSlotCall x False, y)) (\<lambda>(x, y). (FinaliseSlotCall x False, y)) ` inv_image (less_than <*lex*> less_than) (\<lambda>(x, s). case caps_of_state s x of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {x} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0))
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>a b exposed s rv st rva sta aa ba stb stc ab bb std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap (a, b)) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr (aa, ba), stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable aa (a, b); (Inr (), stc) \<in> fst (liftE (set_cap aa (a, b)) stb); (Inr (ab, bb), std) \<in> fst (rec_del (ReduceZombieCall aa (a, b) True) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall aa (a, b) True, stc); exposed\<rbrakk> \<Longrightarrow> (case caps_of_state ste (a, b) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(a, b)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case caps_of_state s (a, b) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(a, b)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final st3 pcap1 pcap2 st4 st5 success cl_info st6 st7. \<lbrakk>(Inr fcap, st2) \<in> fst (liftE (get_cap (oref, cref)) st1); fcap \<noteq> NullCap; (Inr is_final, st3) \<in> fst (liftE (is_final_cap fcap) st2); (Inr (pcap1, pcap2), st4) \<in> fst (liftE (finalise_cap fcap is_final) st3); \<not> cap_removeable pcap1 (oref, cref); (Inr (), st5) \<in> fst (liftE (set_cap pcap1 (oref, cref)) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall pcap1 (oref, cref) True) st5); (Inr (), st7) \<in> fst (preemption_point st6); rec_del_dom (ReduceZombieCall pcap1 (oref, cref) True, st5); exposed\<rbrakk> \<Longrightarrow> (case caps_of_state st7 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case caps_of_state st1 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final st3 pcap1 pcap2 st4 st5 success cl_info st6 st7. \<lbrakk>(Inr fcap, st2) \<in> fst (liftE (get_cap (oref, cref)) st1); fcap \<noteq> NullCap; (Inr is_final, st3) \<in> fst (liftE (is_final_cap fcap) st2); (Inr (pcap1, pcap2), st4) \<in> fst (liftE (finalise_cap fcap is_final) st3); \<not> cap_removeable pcap1 (oref, cref); (Inr (), st5) \<in> fst (liftE (set_cap pcap1 (oref, cref)) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall pcap1 (oref, cref) True) st5); rec_del_dom (ReduceZombieCall pcap1 (oref, cref) True, st5); exposed\<rbrakk> \<Longrightarrow> (case caps_of_state st6 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case caps_of_state st1 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final st3 pcap1 pcap2 st4 st5 success cl_info st6 x111 x112 x113. \<lbrakk>(Inr fcap, st2) \<in> fst (liftE (get_cap (oref, cref)) st1); fcap \<noteq> NullCap; (Inr is_final, st3) \<in> fst (liftE (is_final_cap fcap) st2); (Inr (Zombie x111 x112 x113, pcap2), st4) \<in> fst (liftE (finalise_cap fcap is_final) st3); 0 < x113 \<and> (x111 = oref \<longrightarrow> x113 = Suc 0 \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref); (Inr (), st5) \<in> fst (liftE (set_cap (Zombie x111 x112 x113) (oref, cref)) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall (Zombie x111 x112 x113) (oref, cref) True) st5); rec_del_dom (ReduceZombieCall (Zombie x111 x112 x113) (oref, cref) True, st5); exposed; pcap1 = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case caps_of_state st6 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case caps_of_state st1 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final st3 pcap1 pcap2 st4 st5 success cl_info st6 word option nat. \<lbrakk>(Inr fcap, st2) \<in> fst (liftE (get_cap (oref, cref)) st1); fcap \<noteq> NullCap; (Inr is_final, st3) \<in> fst (liftE (is_final_cap fcap) st2); (Inr (Zombie word option nat, pcap2), st4) \<in> fst (liftE (finalise_cap fcap is_final) st3); 0 < nat \<and> (word = oref \<longrightarrow> nat = Suc 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref); (Inr (), st5) \<in> fst (liftE (set_cap (Zombie word option nat) (oref, cref)) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall (Zombie word option nat) (oref, cref) True) st5); rec_del_dom (ReduceZombieCall (Zombie word option nat) (oref, cref) True, st5); exposed; pcap1 = Zombie word option nat\<rbrakk> \<Longrightarrow> (case caps_of_state st6 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case caps_of_state st1 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final st3 pcap1 pcap2 st4 st5 success cl_info st6 word option nat nata. \<lbrakk>(Inr fcap, st2) \<in> fst (liftE (get_cap (oref, cref)) st1); fcap \<noteq> NullCap; (Inr is_final, st3) \<in> fst (liftE (is_final_cap fcap) st2); (Inr (Zombie word option (Suc nata), pcap2), st4) \<in> fst (liftE (finalise_cap fcap is_final) st3); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (Inr (), st5) \<in> fst (liftE (set_cap (Zombie word option (Suc nata)) (oref, cref)) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True) st5); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True, st5); exposed; pcap1 = Zombie word option (Suc nata); nat = Suc nata\<rbrakk> \<Longrightarrow> (case caps_of_state st6 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case caps_of_state st1 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final st3 pcap2 st4 st5 success cl_info st6 word option nata s'' a s''a b new_cap. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st2); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True, st5); exposed; (Inr (a, b), s'') \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); (new_cap, s''a) \<in> fst (get_cap (oref, cref) s''); (Inr (), st6) \<in> fst ((if new_cap = Zombie word option (Suc nata) then liftE (set_cap (Zombie word option nata) (oref, cref)) else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = (oref, cref) \<and> (word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref))) s''a); (success, cl_info) = undefined\<rbrakk> \<Longrightarrow> (case caps_of_state st6 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case caps_of_state st1 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (4 subgoals):
 1. \<And>oref cref exposed st1 fcap is_final st3 pcap2 st4 st5 success cl_info st6 word option nata s'' a b. \<lbrakk>(success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some fcap; fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st1); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True, st5); exposed; (Inr (a, b), s'') \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); caps_of_state s'' (oref, cref) = Some (Zombie word option (Suc nata)); ((), st6) \<in> fst (set_cap (Zombie word option nata) (oref, cref) s'')\<rbrakk> \<Longrightarrow> (case caps_of_state st6 (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>oref cref exposed st1 fcap is_final st3 pcap2 st4 st5 success cl_info st6 word option nata a b new_cap. \<lbrakk>(success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some fcap; fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st1); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True, st5); exposed; (Inr (a, b), st6) \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); caps_of_state st6 (oref, cref) = Some new_cap; new_cap \<noteq> Zombie word option (Suc nata); new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = (oref, cref) \<and> (word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref)\<rbrakk> \<Longrightarrow> (case new_cap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 3. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 4. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (4 subgoals):
 1. \<And>oref cref exposed st1 fcap is_final st3 pcap2 st4 st5 success cl_info st6 word option nata s'' a b. \<lbrakk>(success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some fcap; fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st1); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True, st5); exposed; (Inr (a, b), s'') \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); caps_of_state s'' (oref, cref) = Some (Zombie word option (Suc nata))\<rbrakk> \<Longrightarrow> (case ((caps_of_state s'')((oref, cref) \<mapsto> Zombie word option nata)) (oref, cref) of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>oref cref exposed st1 fcap is_final st3 pcap2 st4 st5 success cl_info st6 word option nata a b new_cap. \<lbrakk>(success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some fcap; fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st1); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True, st5); exposed; (Inr (a, b), st6) \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); caps_of_state st6 (oref, cref) = Some new_cap; new_cap \<noteq> Zombie word option (Suc nata); new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = (oref, cref) \<and> (word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref)\<rbrakk> \<Longrightarrow> (case new_cap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 3. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 4. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap is_final st3 pcap2 st4 st5 success cl_info st6 word option nata a b new_cap. \<lbrakk>(success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some fcap; fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st1); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True, st5); exposed; (Inr (a, b), st6) \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); caps_of_state st6 (oref, cref) = Some new_cap; new_cap \<noteq> Zombie word option (Suc nata); new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = (oref, cref) \<and> (word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref)\<rbrakk> \<Longrightarrow> (case new_cap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (4 subgoals):
 1. \<And>oref cref exposed st1 fcap is_final st3 pcap2 st4 st5 success cl_info st6 word option nata a b new_cap. \<lbrakk>(success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some fcap; fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st1); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) True, st5); exposed; (Inr (a, b), st6) \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); caps_of_state st6 (oref, cref) = Some NullCap; new_cap = NullCap\<rbrakk> \<Longrightarrow> ((0, 0), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, cref)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than
 2. \<And>oref exposed st1 fcap is_final st3 pcap2 st4 st5 success cl_info st6 word option nata a b new_cap x112 x113. \<lbrakk>(success, cl_info) = undefined; caps_of_state st1 (oref, replicate (zombie_cte_bits x112) False) = Some fcap; fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st1); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, replicate (zombie_cte_bits x112) False) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, replicate (zombie_cte_bits x112) False) True, st5); exposed; (Inr (a, b), st6) \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); caps_of_state st6 (oref, replicate (zombie_cte_bits x112) False) = Some (Zombie oref x112 x113); x112 = option \<longrightarrow> oref = word \<longrightarrow> x113 \<noteq> Suc nata; word = oref \<longrightarrow> zombie_cte_bits option \<noteq> zombie_cte_bits x112; new_cap = Zombie oref x112 x113\<rbrakk> \<Longrightarrow> (fst_cte_ptrs (Zombie oref x112 x113) = {(oref, replicate (zombie_cte_bits x112) False)} \<longrightarrow> ((Suc 0, x113), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, replicate (zombie_cte_bits x112) False)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than) \<and> (fst_cte_ptrs (Zombie oref x112 x113) \<noteq> {(oref, replicate (zombie_cte_bits x112) False)} \<longrightarrow> ((2, x113), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, replicate (zombie_cte_bits x112) False)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than)
 3. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 4. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref exposed st1 fcap is_final st3 pcap2 st4 st5 success cl_info st6 word option nata a b new_cap x112 x113. \<lbrakk>(success, cl_info) = undefined; caps_of_state st1 (oref, replicate (zombie_cte_bits x112) False) = Some fcap; fcap \<noteq> NullCap; (is_final, st3) \<in> fst (is_final_cap fcap st1); ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap is_final st3); ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, replicate (zombie_cte_bits x112) False) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, replicate (zombie_cte_bits x112) False) True, st5); exposed; (Inr (a, b), st6) \<in> fst (rec_del (CTEDeleteCall (word, nat_to_cref (zombie_cte_bits option) nata) False) st5); caps_of_state st6 (oref, replicate (zombie_cte_bits x112) False) = Some (Zombie oref x112 x113); x112 = option \<longrightarrow> oref = word \<longrightarrow> x113 \<noteq> Suc nata; word = oref \<longrightarrow> zombie_cte_bits option \<noteq> zombie_cte_bits x112; new_cap = Zombie oref x112 x113\<rbrakk> \<Longrightarrow> (fst_cte_ptrs (Zombie oref x112 x113) = {(oref, replicate (zombie_cte_bits x112) False)} \<longrightarrow> ((Suc 0, x113), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, replicate (zombie_cte_bits x112) False)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than) \<and> (fst_cte_ptrs (Zombie oref x112 x113) \<noteq> {(oref, replicate (zombie_cte_bits x112) False)} \<longrightarrow> ((2, x113), case fcap of NullCap \<Rightarrow> (0, 0) | Zombie p zb n \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {(oref, replicate (zombie_cte_bits x112) False)} then 1 else 2, n) | _ \<Rightarrow> (3, 0)) \<in> less_than <*lex*> less_than)
 2. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> rec_del_recset
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>slot exposed s rv st rva sta rvb stb stc rvd std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr rvb, stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable (fst rvb) slot; \<not> cap_cyclic_zombie (fst rvb) slot; (Inr (), stc) \<in> fst (liftE (set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall (fst rvb) slot False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> map_prod (\<lambda>(x, y). (FinaliseSlotCall x True, y)) (\<lambda>(x, y). (FinaliseSlotCall x True, y)) ` measure (\<lambda>(x, s). card (not_recursive_cspaces s)) \<or> ((FinaliseSlotCall slot False, ste), FinaliseSlotCall slot False, s) \<in> map_prod (\<lambda>(x, y). (FinaliseSlotCall x False, y)) (\<lambda>(x, y). (FinaliseSlotCall x False, y)) ` measure (\<lambda>(x, s). card (not_recursive_cspaces s))
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>a b exposed s rv st rva sta aa ba stb stc ab bb std ste. \<lbrakk>(Inr rv, st) \<in> fst (liftE (get_cap (a, b)) s); rv \<noteq> NullCap; (Inr rva, sta) \<in> fst (liftE (is_final_cap rv) st); (Inr (aa, ba), stb) \<in> fst (liftE (finalise_cap rv rva) sta); \<not> cap_removeable aa (a, b); \<not> cap_cyclic_zombie aa (a, b); (Inr (), stc) \<in> fst (liftE (set_cap aa (a, b)) stb); (Inr (ab, bb), std) \<in> fst (rec_del (ReduceZombieCall aa (a, b) False) stc); (Inr (), ste) \<in> fst (preemption_point std); rec_del_dom (ReduceZombieCall aa (a, b) False, stc); \<not> exposed\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces ste) < card (not_recursive_cspaces s)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final st3 pcap1 pcap2 st4 st5 success cl_info st6 st7. \<lbrakk>(Inr fcap, st2) \<in> fst (liftE (get_cap (oref, cref)) st1); fcap \<noteq> NullCap; (Inr is_final, st3) \<in> fst (liftE (is_final_cap fcap) st2); (Inr (pcap1, pcap2), st4) \<in> fst (liftE (finalise_cap fcap is_final) st3); \<not> cap_removeable pcap1 (oref, cref); \<not> cap_cyclic_zombie pcap1 (oref, cref); (Inr (), st5) \<in> fst (liftE (set_cap pcap1 (oref, cref)) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall pcap1 (oref, cref) False) st5); (Inr (), st7) \<in> fst (preemption_point st6); rec_del_dom (ReduceZombieCall pcap1 (oref, cref) False, st5); \<not> exposed\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st7) < card (not_recursive_cspaces st1)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final pcap1 pcap2 st4 st5 success cl_info st6 st7. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; is_final = is_final_cap' fcap st2; ((pcap1, pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st2) st2); \<not> cap_removeable pcap1 (oref, cref); \<not> cap_cyclic_zombie pcap1 (oref, cref); ((), st5) \<in> fst (set_cap pcap1 (oref, cref) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall pcap1 (oref, cref) False) st5); (Inr (), st7) \<in> fst (preemption_point st6); rec_del_dom (ReduceZombieCall pcap1 (oref, cref) False, st5); \<not> exposed\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st7) < card (not_recursive_cspaces st1)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final pcap1 pcap2 st4 st5 success cl_info st6 st7. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; is_final = is_final_cap' fcap st2; ((pcap1, pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st2) st2); \<not> cap_removeable pcap1 (oref, cref); \<not> cap_cyclic_zombie pcap1 (oref, cref); ((), st5) \<in> fst (set_cap pcap1 (oref, cref) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall pcap1 (oref, cref) False) st5); rec_del_dom (ReduceZombieCall pcap1 (oref, cref) False, st5); \<not> exposed\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st6) < card (not_recursive_cspaces st1)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final pcap1 pcap2 st4 st5 success cl_info st6 x111 x112 x113. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; is_final = is_final_cap' fcap st2; ((Zombie x111 x112 x113, pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st2) st2); 0 < x113 \<and> (x111 = oref \<longrightarrow> x113 = Suc 0 \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref); \<not> cap_cyclic_zombie (Zombie x111 x112 x113) (oref, cref); ((), st5) \<in> fst (set_cap (Zombie x111 x112 x113) (oref, cref) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall (Zombie x111 x112 x113) (oref, cref) False) st5); rec_del_dom (ReduceZombieCall (Zombie x111 x112 x113) (oref, cref) False, st5); \<not> exposed; pcap1 = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st6) < card (not_recursive_cspaces st1)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final pcap1 pcap2 st4 st5 success cl_info st6 word option nat. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; is_final = is_final_cap' fcap st2; ((Zombie word option nat, pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st2) st2); 0 < nat \<and> (word = oref \<longrightarrow> nat = Suc 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref); \<not> cap_cyclic_zombie (Zombie word option nat) (oref, cref); ((), st5) \<in> fst (set_cap (Zombie word option nat) (oref, cref) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall (Zombie word option nat) (oref, cref) False) st5); rec_del_dom (ReduceZombieCall (Zombie word option nat) (oref, cref) False, st5); \<not> exposed; pcap1 = Zombie word option nat\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st6) < card (not_recursive_cspaces st1)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 is_final pcap1 pcap2 st4 st5 success cl_info st6 word option nat nata. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; is_final = is_final_cap' fcap st2; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st2) st2); word = oref \<longrightarrow> nata = 0 \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); (Inr (success, cl_info), st6) \<in> fst (rec_del (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False) st5); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; pcap1 = Zombie word option (Suc nata); nat = Suc nata\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st6) < card (not_recursive_cspaces st1)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 pcap2 st4 st5 success cl_info st6 word option nata. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st2) st2); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; ((), st6) \<in> fst (cap_swap_for_delete (word, replicate (zombie_cte_bits option) False) (oref, cref) st5); (success, cl_info) = undefined\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st6) < card (not_recursive_cspaces st1)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 pcap2 st4 st5 success cl_info st6 word option nata. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st2) st2); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st5) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap st5 \<and> (word, replicate (zombie_cte_bits option) False) \<in> fst_cte_ptrs cap) (oref, cref) st5 \<and> (word, replicate (zombie_cte_bits option) False) \<noteq> (oref, cref)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st2 pcap2 st4 st5 success cl_info st6 word option nata. \<lbrakk>(fcap, st2) \<in> fst (get_cap (oref, cref) st1); fcap \<noteq> NullCap; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st2) st2); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = fcap) (oref, cref) st2\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st5) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap st5 \<and> (word, replicate (zombie_cte_bits option) False) \<in> fst_cte_ptrs cap) (oref, cref) st5 \<and> (word, replicate (zombie_cte_bits option) False) \<noteq> (oref, cref)
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap pcap2 st4 st5 success cl_info word option nata. \<lbrakk>fcap \<noteq> NullCap; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st1) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); ((), st5) \<in> fst (set_cap (Zombie word option (Suc nata)) (oref, cref) st4); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = fcap) (oref, cref) st1\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st5) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap st5 \<and> (word, replicate (zombie_cte_bits option) False) \<in> fst_cte_ptrs cap) (oref, cref) st5
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap pcap2 st4 st5 success cl_info word option nata. \<lbrakk>fcap \<noteq> NullCap; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st1) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = fcap) (oref, cref) st1\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>cap. fst_cte_ptrs cap = fst_cte_ptrs (Zombie word option (Suc nata))) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1)) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs cap \<and> is_final_cap' cap st4 \<and> (word, replicate (zombie_cte_bits option) False) \<in> fst_cte_ptrs (Zombie word option (Suc nata))) (oref, cref) st4
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap pcap2 st4 st5 success cl_info word option nata. \<lbrakk>fcap \<noteq> NullCap; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st1) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = fcap) (oref, cref) st1\<rbrakk> \<Longrightarrow> is_final_cap' fcap st1 \<longrightarrow> is_final_cap' fcap st1 \<and> cte_wp_at ((=) fcap) (?slot287 oref cref exposed st1 fcap pcap2 st4 st5 success cl_info word option nata) st1
 2. \<And>oref cref exposed st1 fcap pcap2 st4 st5 success cl_info word option nata. \<lbrakk>fcap \<noteq> NullCap; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st1) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = fcap) (oref, cref) st1; fst (Zombie word option (Suc nata), pcap2) = NullCap \<and> snd (Zombie word option (Suc nata), pcap2) = (if is_final_cap' fcap st1 then cap_cleanup_opt fcap else NullCap) \<and> (snd (Zombie word option (Suc nata), pcap2) \<noteq> NullCap \<longrightarrow> is_final_cap' fcap st4) \<or> is_zombie (fst (Zombie word option (Suc nata), pcap2)) \<and> is_final_cap' fcap st4 \<and> is_final_cap' (fst (Zombie word option (Suc nata), pcap2)) st4 \<and> snd (Zombie word option (Suc nata), pcap2) = NullCap \<and> appropriate_cte_cap (fst (Zombie word option (Suc nata), pcap2)) = appropriate_cte_cap fcap \<and> cte_refs (fst (Zombie word option (Suc nata), pcap2)) = cte_refs fcap \<and> gen_obj_refs (fst (Zombie word option (Suc nata), pcap2)) = gen_obj_refs fcap \<and> obj_size (fst (Zombie word option (Suc nata), pcap2)) = obj_size fcap \<and> fst_cte_ptrs (fst (Zombie word option (Suc nata), pcap2)) = fst_cte_ptrs fcap \<and> vs_cap_ref fcap = None\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>cap. fst_cte_ptrs cap = fst_cte_ptrs (Zombie word option (Suc nata))) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1)) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs cap \<and> is_final_cap' cap st4 \<and> (word, replicate (zombie_cte_bits option) False) \<in> fst_cte_ptrs (Zombie word option (Suc nata))) (oref, cref) st4
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap pcap2 st4 st5 success cl_info word option nata. \<lbrakk>fcap \<noteq> NullCap; ((Zombie word option (Suc nata), pcap2), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st1) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = fcap) (oref, cref) st1; fst (Zombie word option (Suc nata), pcap2) = NullCap \<and> snd (Zombie word option (Suc nata), pcap2) = (if is_final_cap' fcap st1 then cap_cleanup_opt fcap else NullCap) \<and> (snd (Zombie word option (Suc nata), pcap2) \<noteq> NullCap \<longrightarrow> is_final_cap' fcap st4) \<or> is_zombie (fst (Zombie word option (Suc nata), pcap2)) \<and> is_final_cap' fcap st4 \<and> is_final_cap' (fst (Zombie word option (Suc nata), pcap2)) st4 \<and> snd (Zombie word option (Suc nata), pcap2) = NullCap \<and> appropriate_cte_cap (fst (Zombie word option (Suc nata), pcap2)) = appropriate_cte_cap fcap \<and> cte_refs (fst (Zombie word option (Suc nata), pcap2)) = cte_refs fcap \<and> gen_obj_refs (fst (Zombie word option (Suc nata), pcap2)) = gen_obj_refs fcap \<and> obj_size (fst (Zombie word option (Suc nata), pcap2)) = obj_size fcap \<and> fst_cte_ptrs (fst (Zombie word option (Suc nata), pcap2)) = fst_cte_ptrs fcap \<and> vs_cap_ref fcap = None\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>cap. fst_cte_ptrs cap = fst_cte_ptrs (Zombie word option (Suc nata))) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1)) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs cap \<and> is_final_cap' cap st4 \<and> (word, replicate (zombie_cte_bits option) False) \<in> fst_cte_ptrs (Zombie word option (Suc nata))) (oref, cref) st4
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata. \<lbrakk>fcap \<noteq> NullCap; ((Zombie word option (Suc nata), NullCap), st4) \<in> fst (finalise_cap fcap (is_final_cap' fcap st1) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = fcap) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' fcap st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap fcap; cte_refs (Zombie word option (Suc nata)) = cte_refs fcap; gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs fcap; (case option of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size fcap; fst_cte_ptrs (Zombie word option (Suc nata)) = fst_cte_ptrs fcap; vs_cap_ref fcap = None\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. fst_cte_ptrs cap = fst_cte_ptrs fcap) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs fcap = gen_obj_refs cap \<and> is_final_cap' cap st4 \<and> (word, replicate (zombie_cte_bits option) False) \<in> fst_cte_ptrs fcap) (oref, cref) st4
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (4 subgoals):
 1. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x61 x63. \<lbrakk>((Zombie x61 option (Suc nata), NullCap), st4) \<in> fst (return (if is_final_cap' (CNodeCap x61 (zombie_cte_bits option) x63) st1 then Zombie x61 (Some (zombie_cte_bits option)) (2 ^ zombie_cte_bits option) else NullCap, NullCap) st1); \<not> cap_cyclic_zombie (Zombie x61 option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie x61 option (Suc nata)) (oref, cref) False, st5); \<not> exposed; x61 = oref \<longrightarrow> replicate (zombie_cte_bits option) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = CNodeCap x61 (zombie_cte_bits option) x63) (oref, cref) st1; is_zombie (Zombie x61 option (Suc nata)); is_final_cap' (CNodeCap x61 (zombie_cte_bits option) x63) st4; is_final_cap' (Zombie x61 option (Suc nata)) st4; appropriate_cte_cap (Zombie x61 option (Suc nata)) = appropriate_cte_cap (CNodeCap x61 (zombie_cte_bits option) x63); cte_refs (Zombie x61 option (Suc nata)) = cte_refs (CNodeCap x61 (zombie_cte_bits option) x63); gen_obj_refs (Zombie x61 option (Suc nata)) = gen_obj_refs (CNodeCap x61 (zombie_cte_bits option) x63); (case option of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = 2 ^ (cte_level_bits + zombie_cte_bits option); word = x61; vs_cap_ref (CNodeCap x61 (zombie_cte_bits option) x63) = None; fcap = CNodeCap x61 (zombie_cte_bits option) x63\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(x61, replicate (zombie_cte_bits option) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (CNodeCap x61 (zombie_cte_bits option) x63) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 2. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- when (is_final_cap' (ThreadCap word) st1) (unbind_notification word);
y <- when (is_final_cap' (ThreadCap word) st1) (suspend word);
y <- when (is_final_cap' (ThreadCap word) st1) (prepare_thread_delete word);
return (if is_final_cap' (ThreadCap word) st1 then Zombie word None 5 else NullCap, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> tcb_cnode_index 0 \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = ThreadCap word) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (ThreadCap word) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (ThreadCap word); cte_refs (Zombie word option (Suc nata)) = cte_refs (ThreadCap word); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (ThreadCap word); (case option of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = 0x200; replicate (zombie_cte_bits option) False = tcb_cnode_index 0; vs_cap_ref (ThreadCap word) = None; fcap = ThreadCap word\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, tcb_cnode_index 0)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (ThreadCap word) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 3. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 4. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- when (is_final_cap' (ThreadCap word) st1) (unbind_notification word);
y <- when (is_final_cap' (ThreadCap word) st1) (suspend word);
y <- when (is_final_cap' (ThreadCap word) st1) (prepare_thread_delete word);
return (if is_final_cap' (ThreadCap word) st1 then Zombie word None 5 else NullCap, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> tcb_cnode_index 0 \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = ThreadCap word) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (ThreadCap word) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (ThreadCap word); cte_refs (Zombie word option (Suc nata)) = cte_refs (ThreadCap word); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (ThreadCap word); (case option of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = 0x200; replicate (zombie_cte_bits option) False = tcb_cnode_index 0; vs_cap_ref (ThreadCap word) = None; fcap = ThreadCap word\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, tcb_cnode_index 0)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (ThreadCap word) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 2. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 st4 st5 success cl_info word s'' s''a. \<lbrakk>\<not> cap_cyclic_zombie (Zombie word None 5) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word None 5) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> tcb_cnode_index 0 \<noteq> cref; (success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some (ThreadCap word); is_zombie (Zombie word None 5); is_final_cap' (ThreadCap word) st4; is_final_cap' (Zombie word None 5) st4; appropriate_cte_cap (Zombie word None 5) = appropriate_cte_cap (ThreadCap word); cte_refs (Zombie word None 5) = cte_refs (ThreadCap word); gen_obj_refs (Zombie word None 5) = gen_obj_refs (ThreadCap word); [False, False, False] = tcb_cnode_index 0; vs_cap_ref (ThreadCap word) = None; is_final_cap' (ThreadCap word) st1; ((), s'') \<in> fst (unbind_notification word st1); ((), s''a) \<in> fst (suspend word s''); ((), st4) \<in> fst (prepare_thread_delete word s''a)\<rbrakk> \<Longrightarrow> (\<exists>cap. caps_of_state st4 (oref, cref) = Some cap \<and> (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, tcb_cnode_index 0)}) \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> (\<exists>cap. caps_of_state st4 (oref, cref) = Some cap \<and> gen_obj_refs (ThreadCap word) = gen_obj_refs cap \<and> is_final_cap' cap st4)
 2. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 st4 st5 success cl_info word s'' s''a. \<lbrakk>\<not> cap_cyclic_zombie (Zombie word None 5) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word None 5) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> tcb_cnode_index 0 \<noteq> cref; (success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some (ThreadCap word); is_zombie (Zombie word None 5); is_final_cap' (ThreadCap word) st4; is_final_cap' (Zombie word None 5) st4; appropriate_cte_cap (Zombie word None 5) = appropriate_cte_cap (ThreadCap word); cte_refs (Zombie word None 5) = cte_refs (ThreadCap word); gen_obj_refs (Zombie word None 5) = gen_obj_refs (ThreadCap word); [False, False, False] = tcb_cnode_index 0; vs_cap_ref (ThreadCap word) = None; is_final_cap' (ThreadCap word) st1; ((), s'') \<in> fst (unbind_notification word st1); ((), s''a) \<in> fst (suspend word s''); ((), st4) \<in> fst (prepare_thread_delete word s''a); caps_of_state s'' (oref, cref) = Some (ThreadCap word); caps_of_state s''a (oref, cref) = Some (ThreadCap word); caps_of_state st4 (oref, cref) = Some (ThreadCap word)\<rbrakk> \<Longrightarrow> (\<exists>cap. caps_of_state st4 (oref, cref) = Some cap \<and> (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, tcb_cnode_index 0)}) \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> (\<exists>cap. caps_of_state st4 (oref, cref) = Some cap \<and> gen_obj_refs (ThreadCap word) = gen_obj_refs cap \<and> is_final_cap' cap st4)
 2. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 st4 st5 success cl_info word s'' s''a. \<lbrakk>\<not> cap_cyclic_zombie (Zombie word None 5) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word None 5) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> tcb_cnode_index 0 \<noteq> cref; (success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some (ThreadCap word); is_zombie (Zombie word None 5); is_final_cap' (ThreadCap word) st4; is_final_cap' (Zombie word None 5) st4; appropriate_cte_cap (Zombie word None 5) = appropriate_cte_cap (ThreadCap word); cte_refs (Zombie word None 5) = cte_refs (ThreadCap word); gen_obj_refs (Zombie word None 5) = gen_obj_refs (ThreadCap word); [False, False, False] = tcb_cnode_index 0; vs_cap_ref (ThreadCap word) = None; is_final_cap' (ThreadCap word) st1; ((), s'') \<in> fst (unbind_notification word st1); ((), s''a) \<in> fst (suspend word s''); ((), st4) \<in> fst (prepare_thread_delete word s''a); caps_of_state s'' (oref, cref) = Some (ThreadCap word); caps_of_state s''a (oref, cref) = Some (ThreadCap word); caps_of_state st4 (oref, cref) = Some (ThreadCap word)\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1)
 2. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 st4 st5 success cl_info word s'' s''a. \<lbrakk>\<not> cap_cyclic_zombie (Zombie word None 5) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word None 5) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> tcb_cnode_index 0 \<noteq> cref; (success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some (ThreadCap word); is_zombie (Zombie word None 5); is_final_cap' (ThreadCap word) st4; is_final_cap' (Zombie word None 5) st4; appropriate_cte_cap (Zombie word None 5) = appropriate_cte_cap (ThreadCap word); cte_refs (Zombie word None 5) = cte_refs (ThreadCap word); gen_obj_refs (Zombie word None 5) = gen_obj_refs (ThreadCap word); [False, False, False] = tcb_cnode_index 0; vs_cap_ref (ThreadCap word) = None; is_final_cap' (ThreadCap word) st1; ((), s'') \<in> fst (unbind_notification word st1); ((), s''a) \<in> fst (suspend word s''); caps_of_state s'' (oref, cref) = Some (ThreadCap word); caps_of_state s''a (oref, cref) = Some (ThreadCap word); caps_of_state st4 (oref, cref) = Some (ThreadCap word)\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces s''a) \<le> card (not_recursive_cspaces st1)
 2. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 st4 st5 success cl_info word s'' s''a. \<lbrakk>\<not> cap_cyclic_zombie (Zombie word None 5) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word None 5) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> tcb_cnode_index 0 \<noteq> cref; (success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some (ThreadCap word); is_zombie (Zombie word None 5); is_final_cap' (ThreadCap word) st4; is_final_cap' (Zombie word None 5) st4; appropriate_cte_cap (Zombie word None 5) = appropriate_cte_cap (ThreadCap word); cte_refs (Zombie word None 5) = cte_refs (ThreadCap word); gen_obj_refs (Zombie word None 5) = gen_obj_refs (ThreadCap word); [False, False, False] = tcb_cnode_index 0; vs_cap_ref (ThreadCap word) = None; is_final_cap' (ThreadCap word) st1; ((), s'') \<in> fst (unbind_notification word st1); caps_of_state s'' (oref, cref) = Some (ThreadCap word); caps_of_state s''a (oref, cref) = Some (ThreadCap word); caps_of_state st4 (oref, cref) = Some (ThreadCap word)\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces s'') \<le> card (not_recursive_cspaces st1)
 2. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (3 subgoals):
 1. \<And>oref cref exposed st1 st4 st5 success cl_info word s'' s''a. \<lbrakk>\<not> cap_cyclic_zombie (Zombie word None 5) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word None 5) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> tcb_cnode_index 0 \<noteq> cref; (success, cl_info) = undefined; caps_of_state st1 (oref, cref) = Some (ThreadCap word); is_zombie (Zombie word None 5); is_final_cap' (ThreadCap word) st4; is_final_cap' (Zombie word None 5) st4; appropriate_cte_cap (Zombie word None 5) = appropriate_cte_cap (ThreadCap word); cte_refs (Zombie word None 5) = cte_refs (ThreadCap word); gen_obj_refs (Zombie word None 5) = gen_obj_refs (ThreadCap word); [False, False, False] = tcb_cnode_index 0; vs_cap_ref (ThreadCap word) = None; is_final_cap' (ThreadCap word) st1; caps_of_state s'' (oref, cref) = Some (ThreadCap word); caps_of_state s''a (oref, cref) = Some (ThreadCap word); caps_of_state st4 (oref, cref) = Some (ThreadCap word)\<rbrakk> \<Longrightarrow> card (not_recursive_cspaces st1) \<le> card (not_recursive_cspaces st1)
 2. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 3. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (2 subgoals):
 1. \<And>oref cref exposed st1 fcap st4 st5 success cl_info word option nata x112 x113. \<lbrakk>((Zombie word option (Suc nata), NullCap), st4) \<in> fst ((do y <- assert (is_final_cap' (Zombie word x112 x113) st1);
return (Zombie word x112 x113, NullCap)
od) st1); \<not> cap_cyclic_zombie (Zombie word option (Suc nata)) (oref, cref); rec_del_dom (ReduceZombieCall (Zombie word option (Suc nata)) (oref, cref) False, st5); \<not> exposed; word = oref \<longrightarrow> replicate (zombie_cte_bits x112) False \<noteq> cref; (success, cl_info) = undefined; cte_wp_at (\<lambda>c. c = Zombie word x112 x113) (oref, cref) st1; is_zombie (Zombie word option (Suc nata)); is_final_cap' (Zombie word x112 x113) st4; is_final_cap' (Zombie word option (Suc nata)) st4; appropriate_cte_cap (Zombie word option (Suc nata)) = appropriate_cte_cap (Zombie word x112 x113); cte_refs (Zombie word option (Suc nata)) = cte_refs (Zombie word x112 x113); gen_obj_refs (Zombie word option (Suc nata)) = gen_obj_refs (Zombie word x112 x113); (case option 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 option = zombie_cte_bits x112; vs_cap_ref (Zombie word x112 x113) = None; fcap = Zombie word x112 x113\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. (case cap of CNodeCap r bits guard \<Rightarrow> {(r, replicate bits False)} | ThreadCap r \<Rightarrow> {(r, tcb_cnode_index 0)} | Zombie r zb n \<Rightarrow> {(r, replicate (zombie_cte_bits zb) False)} | _ \<Rightarrow> {}) = {(word, replicate (zombie_cte_bits x112) False)}) (oref, cref) st4 \<and> card (not_recursive_cspaces st4) \<le> card (not_recursive_cspaces st1) \<and> cte_wp_at (\<lambda>cap. gen_obj_refs (Zombie word x112 x113) = gen_obj_refs cap \<and> is_final_cap' cap st4) (oref, cref) st4
 2. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal (1 subgoal):
 1. \<And>ptr bits n slot s rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ((CTEDeleteCall rv False, st), ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s) \<in> rec_del_recset proof (prove)
goal:
No subgoals!