theory Finalise_DR

lemma delete_cap_one_shrink_descendants:
  "\<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres) \<rbrace> cap_delete_one slot
    \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and>
    CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres) \<rbrace>" including no_pre supply if_cong[cong] apply (simp add:cap_delete_one_def unless_def) apply wp apply (clarsimp simp add:empty_slot_def) apply (wp dxo_wp_weak) apply simp apply (rule_tac P="\<lambda>s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s)
          \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
          in hoare_vcg_precond_imp) apply (rule_tac Q ="\<lambda>r s. Q r s \<and>  (mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))" for Q in hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule delete_cdt_slot_shrink_descendants[where y= "cdt pres" and p = p]) apply (rule_tac Q="\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s ) xa" in hoare_vcg_precond_imp) apply (case_tac slot) apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def mdb_cte_at_def) apply (assumption) apply clarsimp+ apply wp+ apply (rule hoare_vcg_conj_lift[where P="\<lambda>s. cdt s = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s) (cdt s)"]) prefer 2 apply (rule hoare_drop_imp) apply wp apply (clarsimp simp:valid_def in_get_cap_cte_wp_at) apply (drule sym) apply clarsimp apply (drule descendants_not_null_cap) apply simp apply (simp add:cte_wp_at_def) apply (wp|simp)+ apply (rule hoare_vcg_conj_lift) apply (rule hoare_strengthen_post[OF invs_mdb_fast_finalise]) apply (clarsimp simp:valid_mdb_def swp_def) apply wp apply (rule hoare_strengthen_post[OF invs_mdb_fast_finalise]) apply (clarsimp simp:valid_mdb_def swp_def) apply wp apply (clarsimp simp:valid_def in_get_cap_cte_wp_at) apply (clarsimp simp:invs_def valid_mdb_def valid_state_def) apply (drule descendants_not_null_cap) apply simp apply (clarsimp simp:cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<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>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap final y. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final y\<rbrace> IpcCancel_A.empty_slot slot cap.NullCap \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 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;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
y <- do_extended_op (empty_slot_ext slot slot_p);
y <- set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od
od \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>cap final capa x xa xb s f. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> (slot \<notin> CSpaceAcc_A.descendants_of p (cdt (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) = (slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))
 2. \<And>cap final capa x xa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B18 cap final capa x xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>\<lambda>xb s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 3. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>?B18 cap final capa x\<rbrace>
 4. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 5. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 6. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 7. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 8. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cap final capa x xa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B18 cap final capa x xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>\<lambda>xb s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 2. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>?B18 cap final capa x\<rbrace>
 3. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 4. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 5. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 6. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 7. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>cap final capa x xa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 cap final capa x xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>\<lambda>xb s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 2. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> ?Q28 cap final capa x xa s
 3. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 4. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 5. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 6. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 7. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 8. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>cap final capa x xa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 cap final capa x xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>\<lambda>r s. ?Q34 cap final capa x xa r s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>cap final capa x xa rv s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; ?Q34 cap final capa x xa rv s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)
 3. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> ?Q28 cap final capa x xa s
 4. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 5. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 6. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 7. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 8. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 9. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>cap final capa x xa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P35 cap final capa x xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>?Q34 cap final capa x xa\<rbrace>
 2. \<And>cap final capa x xa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 cap final capa x xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 3. \<And>cap final capa x xa rv s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; ?Q34 cap final capa x xa rv s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)
 4. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> ?P35 cap final capa x xa s \<and> ?P'35 cap final capa x xa s
 5. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 6. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 7. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 8. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 9. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 10. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>cap final capa x xa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 cap final capa x xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>cap final capa x xa rv s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; (slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)
 3. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> (valid_mdb s \<and> xa = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p xa \<and> xa = cdt pres) \<and> ?P'35 cap final capa x xa s
 4. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 5. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 6. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 7. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 8. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 9. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>cap final capa x xa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; ?P'35 cap final capa x xa s\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) xa
 3. \<And>cap final capa x xa rv s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; (slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)
 4. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> (valid_mdb s \<and> xa = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p xa \<and> xa = cdt pres) \<and> ?P'35 cap final capa x xa s
 5. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 6. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 7. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 8. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 9. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 10. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>cap final capa x xa a b. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; slot = (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) xa\<rbrace> set_cdt ((\<lambda>p. if xa p = Some slot then xa slot else xa p)(slot := None)) \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; ?P'35 cap final capa x xa s\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) xa
 3. \<And>cap final capa x xa rv s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; (slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)
 4. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> (valid_mdb s \<and> xa = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p xa \<and> xa = cdt pres) \<and> ?P'35 cap final capa x xa s
 5. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 6. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 7. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 8. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 9. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 10. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; ?P'35 cap final capa x xa s\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) xa
 2. \<And>cap final capa x xa rv s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; (slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)
 3. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> (valid_mdb s \<and> xa = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p xa \<and> xa = cdt pres) \<and> ?P'35 cap final capa x xa s
 4. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 5. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 6. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 7. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 8. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 9. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>cap final capa x xa rv s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; (slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<and> CSpaceAcc_A.descendants_of p (cdt (s\<lparr>is_original_cap := (is_original_cap s)(slot := False)\<rparr>)) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)
 2. \<And>cap final capa x xa s. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap; valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> (valid_mdb s \<and> xa = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p xa \<and> xa = cdt pres) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) xa
 3. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 4. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 5. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 6. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 7. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 8. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cap final capa x. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap final capa x\<rbrace> gets cdt \<lbrace>\<lambda>xa s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>cap final capa. \<lbrakk>cap \<noteq> cap.NullCap; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap final capa\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B17 cap final capa\<rbrace>
 3. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> ?R15 cap final capa s)\<rbrace>
 4. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 5. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 6. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B3 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. (capa = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)) \<and> (capa \<noteq> cap.NullCap \<longrightarrow> valid_mdb s \<and> cdt s = cdt s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>?B3 cap final\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cdt s = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. rv = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P'88 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> valid_mdb s \<and> cdt s = cdt s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 3. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> ?P'88 cap final a b\<rbrace>
 4. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 5. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P'88 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> valid_mdb s \<and> cdt s = cdt s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cdt s = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. rv = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 3. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> ?P'88 cap final a b\<rbrace>
 4. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 5. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P'88 cap final ()\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. valid_mdb s \<and> cdt s = cdt s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cdt s = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. rv = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 3. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> ?P'88 cap final a b\<rbrace>
 4. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 5. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cdt s = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. rv = cap.NullCap \<longrightarrow> slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace>
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> valid_mdb b \<and> cdt b = cdt b \<and> cdt pres = cdt b \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt b) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap s. \<lbrakk>cap \<noteq> cap.NullCap; cte_wp_at ((=) cap.NullCap) slot s; cdt s = cdt pres; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt pres); slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> valid_mdb b \<and> cdt b = cdt b \<and> cdt pres = cdt b \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt b) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap s. \<lbrakk>cap \<noteq> cap.NullCap; cte_wp_at ((=) cap.NullCap) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt pres); slot \<in> CSpaceAcc_A.descendants_of p (cdt pres); cdt pres = cdt s\<rbrakk> \<Longrightarrow> False
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> valid_mdb b \<and> cdt b = cdt b \<and> cdt pres = cdt b \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt b) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap s. \<lbrakk>cap \<noteq> cap.NullCap; cte_wp_at ((=) cap.NullCap) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); slot \<in> CSpaceAcc_A.descendants_of p (cdt s); cdt pres = cdt s\<rbrakk> \<Longrightarrow> False
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> valid_mdb b \<and> cdt b = cdt b \<and> cdt pres = cdt b \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt b) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap s. \<lbrakk>cap \<noteq> cap.NullCap; cte_wp_at ((=) cap.NullCap) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt pres = cdt s\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at (?P109 cap s)) s) (cdt s)
 2. \<And>cap s. \<lbrakk>cap \<noteq> cap.NullCap; cte_wp_at ((=) cap.NullCap) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt pres = cdt s; cte_wp_at (?P109 cap s) slot s\<rbrakk> \<Longrightarrow> False
 3. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> valid_mdb b \<and> cdt b = cdt b \<and> cdt pres = cdt b \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt b) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)\<rbrace>
 4. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 5. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap s. \<lbrakk>cap \<noteq> cap.NullCap; cte_wp_at ((=) cap.NullCap) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt pres = cdt s; cte_wp_at ((\<noteq>) cap.NullCap) slot s\<rbrakk> \<Longrightarrow> False
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> valid_mdb b \<and> cdt b = cdt b \<and> cdt pres = cdt b \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt b) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?B2 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>a b. (cdt b = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)) \<and> valid_mdb b \<and> cdt b = cdt b \<and> cdt pres = cdt b \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt b) \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)\<rbrace>
 2. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>?B2 cap\<rbrace>
 3. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P'114 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>rv s. mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> valid_mdb s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)\<rbrace>
 2. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>\<lambda>final s. cdt s = cdt pres \<and> ?P'114 cap final s\<rbrace>
 3. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P118 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>rv s. mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)\<rbrace>
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P'118 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>rv s. valid_mdb s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>\<lambda>final s. cdt s = cdt pres \<and> ?P118 cap final s \<and> ?P'118 cap final s\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap final rv s. \<lbrakk>cap \<noteq> cap.NullCap; valid_mdb s\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)
 2. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P'118 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>rv s. valid_mdb s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)\<rbrace>
 3. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>\<lambda>final s. cdt s = cdt pres \<and> invs s \<and> ?P'118 cap final s\<rbrace>
 4. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P'118 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>rv s. valid_mdb s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)\<rbrace>
 2. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>\<lambda>final s. cdt s = cdt pres \<and> invs s \<and> ?P'118 cap final s\<rbrace>
 3. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap final. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?P'130 cap final\<rbrace> IpcCancel_A.fast_finalise cap final \<lbrace>\<lambda>rv s. mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)\<rbrace>
 2. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>\<lambda>final s. cdt s = cdt pres \<and> invs s \<and> invs s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> ?P'130 cap final s\<rbrace>
 3. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap final rv s. \<lbrakk>cap \<noteq> cap.NullCap; valid_mdb s\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)
 2. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>\<lambda>final s. cdt s = cdt pres \<and> invs s \<and> invs s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> invs s\<rbrace>
 3. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q1 cap\<rbrace> IpcCancel_A.is_final_cap cap \<lbrace>\<lambda>final s. cdt s = cdt pres \<and> invs s \<and> invs s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> invs s\<rbrace>
 2. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then ?Q1 cap else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> cap.NullCap then \<lambda>s. cdt s = cdt pres \<and> invs s \<and> invs s \<and> cdt pres = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) \<and> invs s else (\<lambda>s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot pres; invs pres; slot \<in> CSpaceAcc_A.descendants_of p (cdt pres)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot pres; slot \<in> CSpaceAcc_A.descendants_of p (cdt pres); valid_pspace pres; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) pres) (cdt pres); untyped_mdb (cdt pres) (caps_of_state pres); descendants_inc (cdt pres) (caps_of_state pres); no_mloop (cdt pres); untyped_inc (cdt pres) (caps_of_state pres); ut_revocable (is_original_cap pres) (caps_of_state pres); irq_revocable (is_original_cap pres) (caps_of_state pres); reply_master_revocable (is_original_cap pres) (caps_of_state pres); reply_mdb (cdt pres) (caps_of_state pres); valid_ioc pres; valid_idle pres; only_idle pres; if_unsafe_then_cap pres; valid_reply_caps pres; valid_reply_masters pres; valid_global_refs pres; valid_arch_state pres; valid_irq_node pres; valid_irq_handlers pres; valid_irq_states pres; valid_machine_state pres; valid_vspace_objs pres; valid_arch_caps pres; valid_global_objs pres; valid_kernel_mappings pres; equal_kernel_mappings pres; valid_asid_map pres; valid_global_vspace_mappings pres; pspace_in_kernel_window pres; cap_refs_in_kernel_window pres; pspace_respects_device_region pres; cap_refs_respects_device_region pres; cur_tcb pres\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot pres; valid_pspace pres; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) pres) (cdt pres); untyped_mdb (cdt pres) (caps_of_state pres); descendants_inc (cdt pres) (caps_of_state pres); no_mloop (cdt pres); untyped_inc (cdt pres) (caps_of_state pres); ut_revocable (is_original_cap pres) (caps_of_state pres); irq_revocable (is_original_cap pres) (caps_of_state pres); reply_master_revocable (is_original_cap pres) (caps_of_state pres); reply_mdb (cdt pres) (caps_of_state pres); valid_ioc pres; valid_idle pres; only_idle pres; if_unsafe_then_cap pres; valid_reply_caps pres; valid_reply_masters pres; valid_global_refs pres; valid_arch_state pres; valid_irq_node pres; valid_irq_handlers pres; valid_irq_states pres; valid_machine_state pres; valid_vspace_objs pres; valid_arch_caps pres; valid_global_objs pres; valid_kernel_mappings pres; equal_kernel_mappings pres; valid_asid_map pres; valid_global_vspace_mappings pres; pspace_in_kernel_window pres; cap_refs_in_kernel_window pres; pspace_respects_device_region pres; cap_refs_respects_device_region pres; cur_tcb pres\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ?P182) pres) (cdt pres)
 2. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot pres; valid_pspace pres; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) pres) (cdt pres); untyped_mdb (cdt pres) (caps_of_state pres); descendants_inc (cdt pres) (caps_of_state pres); no_mloop (cdt pres); untyped_inc (cdt pres) (caps_of_state pres); ut_revocable (is_original_cap pres) (caps_of_state pres); irq_revocable (is_original_cap pres) (caps_of_state pres); reply_master_revocable (is_original_cap pres) (caps_of_state pres); reply_mdb (cdt pres) (caps_of_state pres); valid_ioc pres; valid_idle pres; only_idle pres; if_unsafe_then_cap pres; valid_reply_caps pres; valid_reply_masters pres; valid_global_refs pres; valid_arch_state pres; valid_irq_node pres; valid_irq_handlers pres; valid_irq_states pres; valid_machine_state pres; valid_vspace_objs pres; valid_arch_caps pres; valid_global_objs pres; valid_kernel_mappings pres; equal_kernel_mappings pres; valid_asid_map pres; valid_global_vspace_mappings pres; pspace_in_kernel_window pres; cap_refs_in_kernel_window pres; pspace_respects_device_region pres; cap_refs_respects_device_region pres; cur_tcb pres; cte_wp_at ?P182 slot pres\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap.NullCap) slot pres; valid_pspace pres; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) pres) (cdt pres); untyped_mdb (cdt pres) (caps_of_state pres); descendants_inc (cdt pres) (caps_of_state pres); no_mloop (cdt pres); untyped_inc (cdt pres) (caps_of_state pres); ut_revocable (is_original_cap pres) (caps_of_state pres); irq_revocable (is_original_cap pres) (caps_of_state pres); reply_master_revocable (is_original_cap pres) (caps_of_state pres); reply_mdb (cdt pres) (caps_of_state pres); valid_ioc pres; valid_idle pres; only_idle pres; if_unsafe_then_cap pres; valid_reply_caps pres; valid_reply_masters pres; valid_global_refs pres; valid_arch_state pres; valid_irq_node pres; valid_irq_handlers pres; valid_irq_states pres; valid_machine_state pres; valid_vspace_objs pres; valid_arch_caps pres; valid_global_objs pres; valid_kernel_mappings pres; equal_kernel_mappings pres; valid_asid_map pres; valid_global_vspace_mappings pres; pspace_in_kernel_window pres; cap_refs_in_kernel_window pres; pspace_respects_device_region pres; cap_refs_respects_device_region pres; cur_tcb pres; cte_wp_at ((\<noteq>) cap.NullCap) slot pres\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!