theory Interrupt_DR

lemma cte_wp_at_neq_slot_cap_delete_one:
  "slot\<noteq> slot' \<Longrightarrow> \<lbrace>cte_wp_at P slot\<rbrace> cap_delete_one slot'
            \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>" supply send_signal_interrupt_states [wp_unsafe del] validNF_prop [wp_unsafe del] apply (clarsimp simp:cap_delete_one_def unless_def) apply (wp when_wp) apply (clarsimp simp:empty_slot_def) apply (wp cte_wp_at_neq_slot_set_cap) apply clarsimp apply (wp dxo_wp_weak | simp)+ apply (clarsimp simp:set_cdt_def) apply (wp | clarsimp)+ apply (rule_tac Q = "\<lambda>r s. cte_wp_at P slot s \<and> cte_at slot' s" in hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply wp apply (wp get_cap_cte) apply (clarsimp|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot \<noteq> slot' \<Longrightarrow> \<lbrace>cte_wp_at P slot\<rbrace> cap_delete_one slot' \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. slot \<noteq> slot' \<Longrightarrow> \<lbrace>cte_wp_at P slot\<rbrace> cap_delete_one slot' \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. slot \<noteq> slot' \<Longrightarrow> \<lbrace>cte_wp_at P slot\<rbrace> do cap <- CSpaceAcc_A.get_cap slot';
when (cap \<noteq> cap.NullCap) (do final <- IpcCancel_A.is_final_cap cap;
y <- IpcCancel_A.fast_finalise cap final;
IpcCancel_A.empty_slot slot' cap.NullCap
od)
od \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap final y. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final y\<rbrace> IpcCancel_A.empty_slot slot' cap.NullCap \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>
 2. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 3. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 4. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 5. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> do cap <- CSpaceAcc_A.get_cap slot';
if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot');
cdt <- gets cdt;
parent <- return $ cdt slot';
set_cdt ((\<lambda>p. if cdt p = Some slot' then parent else cdt p)(slot' := None));
do_extended_op (empty_slot_ext slot' slot_p);
set_original slot' False;
CSpaceAcc_A.set_cap cap.NullCap slot';
post_cap_deletion cap.NullCap
od
od \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>
 2. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 3. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 4. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 5. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (11 subgoals):
 1. \<And>cap final capa x xa xb xc xd. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B19 cap final capa x xa xb xc xd\<rbrace> set_original slot' False \<lbrace>\<lambda>xe. cte_wp_at P slot and cte_wp_at (\<lambda>_. True) slot'\<rbrace>
 2. \<And>cap final capa x xa xb xc. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x xa xb xc\<rbrace> do_extended_op (empty_slot_ext slot' x) \<lbrace>?B19 cap final capa x xa xb xc\<rbrace>
 3. \<And>cap final capa x xa xb. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap final capa x xa xb\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot' then xb else xa p)(slot' := None)) \<lbrace>?B17 cap final capa x xa xb\<rbrace>
 4. \<And>cap final capa x xa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 cap final capa x xa\<rbrace> return $ xa slot' \<lbrace>?B16 cap final capa x xa\<rbrace>
 5. \<And>cap final capa x. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 cap final capa x\<rbrace> gets cdt \<lbrace>?B15 cap final capa x\<rbrace>
 6. \<And>cap final capa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot') \<lbrace>?B14 cap final capa\<rbrace>
 7. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R12 cap final capa s)\<rbrace>
 8. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 9. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 10. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cap final capa x xa xb. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B19 cap final capa x xa xb () ()\<rbrace> set_original slot' False \<lbrace>\<lambda>xe. cte_wp_at P slot and cte_wp_at (\<lambda>_. True) slot'\<rbrace>
 2. \<And>cap final capa x xa xb xc. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x xa xb xc\<rbrace> do_extended_op (empty_slot_ext slot' x) \<lbrace>?B19 cap final capa x xa xb xc\<rbrace>
 3. \<And>cap final capa x xa xb. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap final capa x xa xb\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot' then xb else xa p)(slot' := None)) \<lbrace>?B17 cap final capa x xa xb\<rbrace>
 4. \<And>cap final capa x xa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 cap final capa x xa\<rbrace> return $ xa slot' \<lbrace>?B16 cap final capa x xa\<rbrace>
 5. \<And>cap final capa x. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 cap final capa x\<rbrace> gets cdt \<lbrace>?B15 cap final capa x\<rbrace>
 6. \<And>cap final capa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot') \<lbrace>?B14 cap final capa\<rbrace>
 7. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R12 cap final capa s)\<rbrace>
 8. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 9. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 10. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>cap final capa x xa xb. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap final capa x xa xb\<rbrace> set_cdt (\<lambda>a. if a = slot' then None else if xa a = Some slot' then xb else xa a) \<lbrace>\<lambda>xc a. cte_wp_at P slot a \<and> cte_wp_at (\<lambda>_. True) slot' a\<rbrace>
 2. \<And>cap final capa x xa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 cap final capa x xa\<rbrace> return $ xa slot' \<lbrace>?B16 cap final capa x xa\<rbrace>
 3. \<And>cap final capa x. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 cap final capa x\<rbrace> gets cdt \<lbrace>?B15 cap final capa x\<rbrace>
 4. \<And>cap final capa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot') \<lbrace>?B14 cap final capa\<rbrace>
 5. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R12 cap final capa s)\<rbrace>
 6. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 7. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 8. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 9. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>cap final capa x xa xb. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap final capa x xa xb\<rbrace> do s <- get;
put (s\<lparr>cdt := \<lambda>a. if a = slot' then None else if xa a = Some slot' then xb else xa a\<rparr>)
od \<lbrace>\<lambda>xc a. cte_wp_at P slot a \<and> cte_wp_at (\<lambda>_. True) slot' a\<rbrace>
 2. \<And>cap final capa x xa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B15 cap final capa x xa\<rbrace> return $ xa slot' \<lbrace>?B16 cap final capa x xa\<rbrace>
 3. \<And>cap final capa x. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B14 cap final capa x\<rbrace> gets cdt \<lbrace>?B15 cap final capa x\<rbrace>
 4. \<And>cap final capa. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot') \<lbrace>?B14 cap final capa\<rbrace>
 5. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R12 cap final capa s)\<rbrace>
 6. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 7. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 8. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 9. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s)\<rbrace>
 2. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 3. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 4. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 5. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>r s. cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s\<rbrace>
 2. \<And>cap final rv s. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s\<rbrakk> \<Longrightarrow> (rv = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (rv \<noteq> cap.NullCap \<longrightarrow> cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s)
 3. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 4. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 5. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 6. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P62 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>
 2. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'61 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) slot'\<rbrace>
 3. \<And>cap final rv s. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s\<rbrakk> \<Longrightarrow> (rv = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (rv \<noteq> cap.NullCap \<longrightarrow> cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s)
 4. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. ?P62 cap final a b \<and> ?P'61 cap final a b\<rbrace>
 5. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 6. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 7. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'61 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) slot'\<rbrace>
 2. \<And>cap final rv s. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s\<rbrakk> \<Longrightarrow> (rv = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (rv \<noteq> cap.NullCap \<longrightarrow> cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s)
 3. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. cte_wp_at P slot b \<and> ?P'61 cap final a b\<rbrace>
 4. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 5. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 6. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap final rv s. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap; cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s\<rbrakk> \<Longrightarrow> (rv = cap.NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (rv \<noteq> cap.NullCap \<longrightarrow> cte_wp_at P slot s \<and> cte_wp_at (\<lambda>_. True) slot' s)
 2. \<And>cap final. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. cte_wp_at P slot b \<and> True\<rbrace>
 3. \<And>cap. \<lbrakk>slot \<noteq> slot'; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B3 cap\<rbrace>
 4. slot \<noteq> slot' \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap slot' \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q2 cap else cte_wp_at P slot\<rbrace>
 5. \<And>s. \<lbrakk>slot \<noteq> slot'; cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!