theory CNodeInv_R

lemma cteDelete_cte_wp_at_invs:
  "\<lbrakk> \<And>cap. P cap \<Longrightarrow> isZombie cap \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_to' slot s \<and>
       cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>
     cteDelete slot False
   \<lbrace>\<lambda>rv. cte_at' slot and invs' and sch_act_simple
        and cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = NullCap \<or>
        (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp
             \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p\<rbrace>, -" apply (rule hoare_pre) apply (wp cteDelete_cte_at) prefer 2 apply (erule_tac Q="invs' s \<and> R" for s R in conjI[rotated]) apply simp apply (simp only: cteDelete_def withoutPreemption_def fun_app_def split_def) apply (cases "p = slot") apply (cases "\<exists>cp. P cp") apply (simp add: whenE_def) apply wp apply (rule hoare_strengthen_post [OF emptySlot_deletes]) apply (clarsimp simp: cte_wp_at_ctes_of) apply wp apply (simp add: imp_conjR conj_comms) apply (rule_tac Q="\<lambda>rv s. invs' s \<and> sch_act_simple s \<and>
                   (fst rv \<longrightarrow>
                       cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and>
                   (fst rv \<longrightarrow>
                       (\<forall>sl'. snd rv \<noteq> NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow>
                                  cteCaps_of s sl' \<noteq> Some (snd rv))) \<and>
                   (\<not> fst rv \<longrightarrow>
                       cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or>
                                         cteCap cte = NullCap \<or>
                                         (\<exists>zb n. cteCap cte = Zombie slot zb n))
                                  slot s)"
                and E="\<lambda>rv. \<top>" in hoare_post_impErr) apply (wp finaliseSlot_invs finaliseSlot_removeable finaliseSlot_sch_act_simple
                hoare_drop_imps(2)[OF finaliseSlot_irqs]) apply (rule hoare_post_imp_R, rule finaliseSlot_abort_cases) apply (clarsimp simp: cte_wp_at_ctes_of dest!: isCapDs) apply simp apply simp apply simp apply (simp add: cte_wp_at_ctes_of validE_R_def) apply (simp add: whenE_def) apply (wp emptySlot_cte_wp_cap_other) apply (rule_tac Q'="\<lambda>rv s. invs' s \<and> sch_act_simple s \<and>
                  (fst rv \<longrightarrow>
                      cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and>
                  (fst rv \<longrightarrow>
                      (\<forall>sl'. snd rv \<noteq> NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow>
                                 cteCaps_of s sl' \<noteq> Some (snd rv))) \<and>
                  cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or>
                                    cteCap cte = NullCap \<or>
                                    (\<exists>zb n. cteCap cte = Zombie p zb n) \<and>
                                    (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p))
                             p s"
               in hoare_post_imp_R) apply (wp finaliseSlot_invs finaliseSlot_removeable finaliseSlot_sch_act_simple
              hoare_drop_imps(2)[OF finaliseSlot_irqs]) apply (rule hoare_post_imp_R [OF finaliseSlot_cte_wp_at[where p=p and P=P]]) apply simp+ apply (clarsimp simp: cte_wp_at_ctes_of) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cap. P cap \<Longrightarrow> isZombie cap) \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> cteDelete slot False \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) slot and invs' and sch_act_simple and cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. (\<And>cap. P cap \<Longrightarrow> isZombie cap) \<Longrightarrow> \<lbrace>?P'\<rbrace> cteDelete slot False \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) slot and invs' and sch_act_simple and cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p\<rbrace>, -
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. (\<And>cap. P cap \<Longrightarrow> isZombie cap) \<Longrightarrow> \<lbrace>?P'7\<rbrace> cteDelete slot False \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> ?P'7 s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> ?P'7 s
 2. (\<And>cap. P cap \<Longrightarrow> isZombie cap) \<Longrightarrow> \<lbrace>?P'7\<rbrace> cteDelete slot False \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<And>cap. P cap \<Longrightarrow> isZombie cap) \<Longrightarrow> True
 2. (\<And>cap. P cap \<Longrightarrow> isZombie cap) \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> cteDelete slot False \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (\<And>cap. P cap \<Longrightarrow> isZombie cap) \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> cteDelete slot False \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (\<And>cap. P cap \<Longrightarrow> isZombie cap) \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 2. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 2. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 3. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrace> doE p <- finaliseSlot slot False;
if fst p then liftE (emptySlot slot (snd p)) else returnOk ()
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s\<rbrace>, -
 2. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 3. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<And>pa. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; fst pa\<rbrakk> \<Longrightarrow> \<lbrace>?P'24 pa\<rbrace> emptySlot slot (snd pa) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot\<rbrace>
 2. \<And>pa. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; \<not> fst pa\<rbrakk> \<Longrightarrow> \<lbrace>?R19 pa\<rbrace> returnOk () \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s\<rbrace>, -
 3. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>?P'17\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>p s. (fst p \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd p \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd p))) \<and> sch_act_simple s \<and> ?P'24 p s) \<and> (\<not> fst p \<longrightarrow> ?R19 p s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> ?P'17 s
 5. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 6. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<And>pa rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; fst pa; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s
 2. \<And>pa. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; \<not> fst pa\<rbrakk> \<Longrightarrow> \<lbrace>?R19 pa\<rbrace> returnOk () \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s\<rbrace>, -
 3. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>?P'17\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>p s. (fst p \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd p \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd p))) \<and> sch_act_simple s \<and> True) \<and> (\<not> fst p \<longrightarrow> ?R19 p s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> ?P'17 s
 5. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 6. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>pa. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; \<not> fst pa\<rbrakk> \<Longrightarrow> \<lbrace>?R19 pa\<rbrace> returnOk () \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s\<rbrace>, -
 2. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>?P'17\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>p s. (fst p \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd p \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd p))) \<and> sch_act_simple s \<and> True) \<and> (\<not> fst p \<longrightarrow> ?R19 p s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> ?P'17 s
 4. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 5. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>?P'17\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>p s. (fst p \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd p \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd p))) \<and> sch_act_simple s \<and> True) \<and> (\<not> fst p \<longrightarrow> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> ?P'17 s
 3. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 4. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>?P'17\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>p s. (fst p \<longrightarrow> invs' s) \<and> (fst p \<longrightarrow> sch_act_simple s) \<and> (\<not> fst p \<longrightarrow> invs' s) \<and> (\<not> fst p \<longrightarrow> sch_act_simple s) \<and> (fst p \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst p \<longrightarrow> snd p \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd p))) \<and> (\<not> fst p \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> ?P'17 s
 3. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 4. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>?P'17\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> invs' s) \<and> (fst rv \<longrightarrow> sch_act_simple s) \<and> (\<not> fst rv \<longrightarrow> invs' s) \<and> (\<not> fst rv \<longrightarrow> sch_act_simple s) \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> snd rv \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)
 3. \<And>e s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> ?P'17 s
 5. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 6. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>?P'49\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>rv s. \<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s\<rbrace>, -
 2. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> invs' s) \<and> (fst rv \<longrightarrow> sch_act_simple s) \<and> (\<not> fst rv \<longrightarrow> invs' s) \<and> (\<not> fst rv \<longrightarrow> sch_act_simple s) \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> snd rv \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)
 3. \<And>e s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> ?P'49 s
 5. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 6. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; fst rv \<or> \<not> False \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s\<rbrakk> \<Longrightarrow> \<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s
 2. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> invs' s) \<and> (fst rv \<longrightarrow> sch_act_simple s) \<and> (\<not> fst rv \<longrightarrow> invs' s) \<and> (\<not> fst rv \<longrightarrow> sch_act_simple s) \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> snd rv \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)
 3. \<And>e s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> True
 5. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 6. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> invs' s) \<and> (fst rv \<longrightarrow> sch_act_simple s) \<and> (\<not> fst rv \<longrightarrow> invs' s) \<and> (\<not> fst rv \<longrightarrow> sch_act_simple s) \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> snd rv \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> (\<not> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie slot zb n)) slot s)
 2. \<And>e s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> True
 4. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 5. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>e s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; True\<rbrakk> \<Longrightarrow> True
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> True
 3. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 4. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<exists>cp. P cp; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> True
 2. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 3. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p = slot; \<nexists>cp. P cp\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, -
 2. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
whenE (False \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (capZombiePtr cp \<noteq> p \<or> p = slot))) p s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> doE p <- finaliseSlot slot False;
if fst p then liftE (emptySlot slot (snd p)) else returnOk ()
odE \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'84\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>pa s. (fst pa \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd pa \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd pa))) \<and> sch_act_simple s \<and> (cte_wp_at' (\<lambda>c. P (cteCap c) \<or> cteCap c = capability.NullCap \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p and K (p \<noteq> slot)) s) \<and> (\<not> fst pa \<longrightarrow> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s)\<rbrace>, -
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> ?P'84 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'84\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrace>, -
 2. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> sch_act_simple s \<and> (cte_wp_at' (\<lambda>c. P (cteCap c) \<or> cteCap c = capability.NullCap \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p and K (p \<noteq> slot)) s) \<and> (\<not> fst rv \<longrightarrow> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s)
 3. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> ?P'84 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'94\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p\<rbrace>, -
 2. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> sch_act_simple s \<and> (cte_wp_at' (\<lambda>c. P (cteCap c) \<or> cteCap c = capability.NullCap \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p and K (p \<noteq> slot)) s) \<and> (\<not> fst rv \<longrightarrow> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s)
 3. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> ?P'94 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; P cap\<rbrakk> \<Longrightarrow> isZombie cap
 2. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot
 3. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s
 4. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> sch_act_simple s \<and> (cte_wp_at' (\<lambda>c. P (cteCap c) \<or> cteCap c = capability.NullCap \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p and K (p \<noteq> slot)) s) \<and> (\<not> fst rv \<longrightarrow> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s)
 5. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s
 2. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> sch_act_simple s \<and> (cte_wp_at' (\<lambda>c. P (cteCap c) \<or> cteCap c = capability.NullCap \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p and K (p \<noteq> slot)) s) \<and> (\<not> fst rv \<longrightarrow> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s)
 3. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (fst rv \<longrightarrow> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrakk> \<Longrightarrow> (fst rv \<longrightarrow> (invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))) \<and> sch_act_simple s \<and> (cte_wp_at' (\<lambda>c. P (cteCap c) \<or> cteCap c = capability.NullCap \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p and K (p \<noteq> slot)) s) \<and> (\<not> fst rv \<longrightarrow> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> cteCap cte = capability.NullCap \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s)
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> True \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s proof (prove)
goal:
No subgoals!