theory FinalCaps

lemma finalise_cap_ret_is_silc:
  "\<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb
                    and cte_wp_at ((=) cap) slot and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace>
   finalise_cap cap blah
   \<lbrace>\<lambda>rvb s. \<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot))
            \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (fst rvb) s \<and>
                         pasObjectAbs aag (fst lslot) = SilcLabel)\<rbrace>" apply (clarsimp simp: valid_def) apply (rename_tac a b s') apply (cut_tac aag1=aag and r="(a,b)" and l1="pasObjectAbs aag (fst slot)"
              in hoare_contrapositive[OF finalise_cap_ret_intra_label_cap]) apply simp apply assumption apply (frule use_valid[OF _ finalise_cap_silc_inv[where st=st]]) apply simp apply (frule_tac s=s in silc_invD) apply assumption apply (fastforce simp: intra_label_cap_def) apply (simp, elim exE conjE) apply (rename_tac la lb) apply (rule_tac x=la in exI, simp) apply (rule_tac x=lb in exI) apply (drule_tac lslot="(la,lb)" in silc_inv_preserves_silc_dom_caps, simp+) apply (drule nonempty_refs)+ apply (erule disjE[where P="obj_refs cap \<noteq> {}"]) apply (subgoal_tac "cap_irqs cap = {} \<and> cap_irqs a = {}") apply (clarsimp simp: slots_holding_overlapping_caps_def get_cap_cte_wp_at') apply (rename_tac cap'a) apply (rule_tac x=cap'a in exI) apply simp apply (subgoal_tac "\<exists>x. obj_refs cap = {x} \<and> obj_refs a = {x}") apply blast apply (erule nonemptyE) apply (rename_tac x) apply (rule_tac x=x in exI) apply (subgoal_tac "obj_refs a \<subseteq> obj_refs cap") apply (drule (1) subsetD) apply (blast dest: caps_ref_single_objects) apply (fastforce dest: use_valid[OF _ finalise_cap_ret_subset_obj_refs]) apply (fastforce dest: caps_ref_either_an_object_or_irq
                          use_valid[OF _ finalise_cap_ret_subset_cap_irqs]) apply (subgoal_tac "obj_refs cap = {} \<and> obj_refs a = {}") apply (clarsimp simp: slots_holding_overlapping_caps_def get_cap_cte_wp_at') apply (rename_tac cap'a) apply (rule_tac x=cap'a in exI) apply simp apply (subgoal_tac "\<exists>x. cap_irqs cap = {x} \<and> cap_irqs a = {x}") apply blast apply (erule nonemptyE) apply (rename_tac x) apply (rule_tac x=x in exI) apply (subgoal_tac "cap_irqs a \<subseteq> cap_irqs cap") apply (drule (1) subsetD) apply (blast dest: caps_ref_single_irqs) apply (fastforce dest: use_valid[OF _ finalise_cap_ret_subset_cap_irqs]) apply (fastforce dest: caps_ref_either_an_object_or_irq'
                         use_valid[OF _ finalise_cap_ret_subset_obj_refs]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and cte_wp_at ((=) cap) slot and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rvb s. \<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (fst rvb) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a ba) \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag (fst (a, b)) (pasObjectAbs aag (fst slot))
 2. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> ((a, b), ?s'17 s a b s') \<in> fst (finalise_cap (?cap18 s a b s') (?blah18 s a b s') (?s17 s a b s'))
 3. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag (?cap18 s a b s') (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> ((a, b), ?s'17 s a b s') \<in> fst (finalise_cap (?cap18 s a b s') (?blah18 s a b s') (?s17 s a b s'))
 2. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag (?cap18 s a b s') (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)) s
 2. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap23 s a b s')) (?slot23 s a b s') s
 2. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot23 s a b s') s
 3. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap23 s a b s') s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag slot s
 2. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s a b s'. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s a b s' aa ba. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'; pasObjectAbs aag aa = SilcLabel; (aa, ba) \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s') \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<exists>b. (la, b) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (1 subgoal):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (1 subgoal):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; \<not> cap_points_to_label aag a (pasObjectAbs aag (fst slot)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (1 subgoal):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s'
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}; cap_irqs cap = {} \<and> cap_irqs a = {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s'
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs a \<noteq> {}; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') (la, lb) s' \<and> obj_refs a \<inter> obj_refs cap' \<noteq> {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs a \<noteq> {}; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') (la, lb) s' \<and> obj_refs a \<inter> obj_refs cap' \<noteq> {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs a \<noteq> {}; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap'a) (la, lb) s' \<and> obj_refs a \<inter> obj_refs cap'a \<noteq> {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs a \<noteq> {}; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs a \<inter> obj_refs cap'a \<noteq> {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (4 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs a \<noteq> {}; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; \<exists>x. obj_refs cap = {x} \<and> obj_refs a = {x}\<rbrakk> \<Longrightarrow> obj_refs a \<inter> obj_refs cap'a \<noteq> {}
 2. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs a \<noteq> {}; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x. obj_refs cap = {x} \<and> obj_refs a = {x}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 4. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs a \<noteq> {}; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x. obj_refs cap = {x} \<and> obj_refs a = {x}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; x \<in> obj_refs a\<rbrakk> \<Longrightarrow> \<exists>x. obj_refs cap = {x} \<and> obj_refs a = {x}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; x \<in> obj_refs a\<rbrakk> \<Longrightarrow> \<exists>x. obj_refs cap = {x} \<and> obj_refs a = {x}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; x \<in> obj_refs a\<rbrakk> \<Longrightarrow> obj_refs cap = {x} \<and> obj_refs a = {x}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (4 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; x \<in> obj_refs a; obj_refs a \<subseteq> obj_refs cap\<rbrakk> \<Longrightarrow> obj_refs cap = {x} \<and> obj_refs a = {x}
 2. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; x \<in> obj_refs a\<rbrakk> \<Longrightarrow> obj_refs a \<subseteq> obj_refs cap
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 4. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (4 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; x \<in> obj_refs a; x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> obj_refs cap = {x} \<and> obj_refs a = {x}
 2. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; x \<in> obj_refs a\<rbrakk> \<Longrightarrow> obj_refs a \<subseteq> obj_refs cap
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 4. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; obj_refs cap \<noteq> {}; cap_irqs cap = {}; cap_irqs a = {}; cte_wp_at ((=) cap') (la, lb) s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; obj_refs cap \<inter> obj_refs cap'a \<noteq> {}; x \<in> obj_refs a\<rbrakk> \<Longrightarrow> obj_refs a \<subseteq> obj_refs cap
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap = {} \<and> cap_irqs a = {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (1 subgoal):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s' proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}; obj_refs cap = {} \<and> obj_refs a = {}\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps a s'
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') (la, lb) s' \<and> cap_irqs a \<inter> cap_irqs cap' \<noteq> {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') (la, lb) s' \<and> cap_irqs a \<inter> cap_irqs cap' \<noteq> {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap'a) (la, lb) s' \<and> cap_irqs a \<inter> cap_irqs cap'a \<noteq> {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs a \<inter> cap_irqs cap'a \<noteq> {}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; \<exists>x. cap_irqs cap = {x} \<and> cap_irqs a = {x}\<rbrakk> \<Longrightarrow> cap_irqs a \<inter> cap_irqs cap'a \<noteq> {}
 2. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x. cap_irqs cap = {x} \<and> cap_irqs a = {x}
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x. cap_irqs cap = {x} \<and> cap_irqs a = {x}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; x \<in> cap_irqs a\<rbrakk> \<Longrightarrow> \<exists>x. cap_irqs cap = {x} \<and> cap_irqs a = {x}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; x \<in> cap_irqs a\<rbrakk> \<Longrightarrow> \<exists>x. cap_irqs cap = {x} \<and> cap_irqs a = {x}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; x \<in> cap_irqs a\<rbrakk> \<Longrightarrow> cap_irqs cap = {x} \<and> cap_irqs a = {x}
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; x \<in> cap_irqs a; cap_irqs a \<subseteq> cap_irqs cap\<rbrakk> \<Longrightarrow> cap_irqs cap = {x} \<and> cap_irqs a = {x}
 2. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; x \<in> cap_irqs a\<rbrakk> \<Longrightarrow> cap_irqs a \<subseteq> cap_irqs cap
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (3 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; x \<in> cap_irqs a; x \<in> cap_irqs cap\<rbrakk> \<Longrightarrow> cap_irqs cap = {x} \<and> cap_irqs a = {x}
 2. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; x \<in> cap_irqs a\<rbrakk> \<Longrightarrow> cap_irqs a \<subseteq> cap_irqs cap
 3. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (2 subgoals):
 1. \<And>s a b s' la lb cap' cap'a x. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; cap_irqs cap \<noteq> {}; obj_refs cap = {}; obj_refs a = {}; cte_wp_at ((=) cap') (la, lb) s; cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) (la, lb) s'; cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; x \<in> cap_irqs a\<rbrakk> \<Longrightarrow> cap_irqs a \<subseteq> cap_irqs cap
 2. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal (1 subgoal):
 1. \<And>s a b s' la lb. \<lbrakk>((a, b), s') \<in> fst (finalise_cap cap blah s); pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) cap) slot s; pas_refined aag s; pas_cap_cur_auth aag cap; silc_inv aag st s'; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s; (la, lb) \<in> slots_holding_overlapping_caps cap s'; obj_refs a \<noteq> {} \<or> cap_irqs a \<noteq> {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap = {} \<and> obj_refs a = {} proof (prove)
goal:
No subgoals!