theory FinalCaps

lemma set_cap_slots_holding_overlapping_caps_other:
  "\<lbrace>\<lambda>s. x \<in> slots_holding_overlapping_caps capa s \<and>
        pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot)\<rbrace>
   set_cap cap slot
   \<lbrace>\<lambda>rv s. x \<in> slots_holding_overlapping_caps capa s\<rbrace>" unfolding set_cap_def apply (wpsimp wp: set_object_wp get_object_wp)+ apply (case_tac "obj_refs capa = {} \<and> cap_irqs capa = {}") apply (clarsimp simp: slots_holding_overlapping_caps_def) apply (fastforce simp: get_cap_def get_object_def bind_def split_def gets_def get_def
                          return_def assert_def assert_opt_def fail_def
                   split: kernel_object.splits if_splits option.splits) apply (subgoal_tac "fst x \<noteq> fst slot") apply (intro allI impI conjI) apply (clarsimp simp: slots_holding_overlapping_caps_def) apply (rule_tac x=cap' in exI) apply clarsimp apply (subst get_cap_cte_wp_at') apply (rule upd_other_cte_wp_at) apply (simp add: cte_wp_at_def) apply assumption apply (clarsimp simp: get_cap_caps_of_state) apply ((drule set_cap_slots_holding_overlapping_caps_helper[where slot=slot], simp+)+)[5] apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. x \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot)\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv s. x \<in> slots_holding_overlapping_caps capa s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. x \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot)\<rbrace> case slot of (oref, cref) \<Rightarrow> do obj <- get_object oref;
(case obj of CNode sz cn \<Rightarrow> if cref \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(cref \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object oref
od \<lbrace>\<lambda>rv s. x \<in> slots_holding_overlapping_caps capa s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xaa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xaa = tcb_cnode_index 0 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xaa = tcb_cnode_index (Suc 0) \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xaa = tcb_cnode_index 2 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xaa = tcb_cnode_index 3 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 3 \<longrightarrow> xaa = tcb_cnode_index 4 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)))))) proof (prove)
goal (2 subgoals):
 1. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; obj_refs capa = {} \<and> cap_irqs capa = {}\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xaa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xaa = tcb_cnode_index 0 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xaa = tcb_cnode_index (Suc 0) \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xaa = tcb_cnode_index 2 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xaa = tcb_cnode_index 3 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 3 \<longrightarrow> xaa = tcb_cnode_index 4 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>))))))
 2. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xaa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xaa = tcb_cnode_index 0 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xaa = tcb_cnode_index (Suc 0) \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xaa = tcb_cnode_index 2 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xaa = tcb_cnode_index 3 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 3 \<longrightarrow> xaa = tcb_cnode_index 4 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)))))) proof (prove)
goal (2 subgoals):
 1. \<And>s xa xaa ko cap'. \<lbrakk>pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; obj_refs capa = {}; cap_irqs capa = {}; fst (get_cap x s) = {(cap', s)}; arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xaa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> (\<exists>cap'. fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)} \<and> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {})) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xaa = tcb_cnode_index 0 \<longrightarrow> (\<exists>cap'. fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)} \<and> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {})) \<and> (xaa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xaa = tcb_cnode_index (Suc 0) \<longrightarrow> (\<exists>cap'. fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)} \<and> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {})) \<and> (xaa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xaa = tcb_cnode_index 2 \<longrightarrow> (\<exists>cap'. fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)} \<and> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {})) \<and> (xaa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xaa = tcb_cnode_index 3 \<longrightarrow> (\<exists>cap'. fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)} \<and> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {})) \<and> (xaa \<noteq> tcb_cnode_index 3 \<longrightarrow> xaa = tcb_cnode_index 4 \<longrightarrow> (\<exists>cap'. fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)} \<and> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}))))))
 2. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xaa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xaa = tcb_cnode_index 0 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xaa = tcb_cnode_index (Suc 0) \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xaa = tcb_cnode_index 2 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xaa = tcb_cnode_index 3 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 3 \<longrightarrow> xaa = tcb_cnode_index 4 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xaa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xaa = tcb_cnode_index 0 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xaa = tcb_cnode_index (Suc 0) \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xaa = tcb_cnode_index 2 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xaa = tcb_cnode_index 3 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 3 \<longrightarrow> xaa = tcb_cnode_index 4 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)))))) proof (prove)
goal (2 subgoals):
 1. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xaa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xaa = tcb_cnode_index 0 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xaa = tcb_cnode_index (Suc 0) \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xaa = tcb_cnode_index 2 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xaa = tcb_cnode_index 3 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)) \<and> (xaa \<noteq> tcb_cnode_index 3 \<longrightarrow> xaa = tcb_cnode_index 4 \<longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>))))))
 2. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (7 subgoals):
 1. \<And>s xa xaa ko xb xc. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = CNode xb xc; xaa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)
 2. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 7. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (7 subgoals):
 1. \<And>s xa xaa xb xc cap' y. \<lbrakk>pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at (CNode xb xc) xa s; obj_refs capa = {} \<longrightarrow> cap_irqs capa \<noteq> {}; fst x \<noteq> xa; well_formed_cnode_n xb xc; xc xaa = Some y; fst (get_cap x s) = {(cap', s)}; cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)} \<and> (cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {})
 2. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 7. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (7 subgoals):
 1. \<And>s xa xaa xb xc cap' y. \<lbrakk>pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at (CNode xb xc) xa s; obj_refs capa = {} \<longrightarrow> cap_irqs capa \<noteq> {}; fst x \<noteq> xa; well_formed_cnode_n xb xc; xc xaa = Some y; fst (get_cap x s) = {(cap', s)}; cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)} \<and> (cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {})
 2. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 7. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (7 subgoals):
 1. \<And>s xa xaa xb xc cap' y. \<lbrakk>pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at (CNode xb xc) xa s; obj_refs capa = {} \<longrightarrow> cap_irqs capa \<noteq> {}; fst x \<noteq> xa; well_formed_cnode_n xb xc; xc xaa = Some y; fst (get_cap x s) = {(cap', s)}; cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> fst (get_cap x (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)}
 2. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 7. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (7 subgoals):
 1. \<And>s xa xaa xb xc cap' y. \<lbrakk>pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at (CNode xb xc) xa s; obj_refs capa = {} \<longrightarrow> cap_irqs capa \<noteq> {}; fst x \<noteq> xa; well_formed_cnode_n xb xc; xc xaa = Some y; fst (get_cap x s) = {(cap', s)}; cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') x (s\<lparr>kheap := (kheap s)(xa \<mapsto> CNode xb (\<lambda>a. if a = xaa then Some cap else xc a))\<rparr>)
 2. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 7. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (8 subgoals):
 1. \<And>s xa xaa xb xc cap' y. \<lbrakk>pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at (CNode xb xc) xa s; obj_refs capa = {} \<longrightarrow> cap_irqs capa \<noteq> {}; fst x \<noteq> xa; well_formed_cnode_n xb xc; xc xaa = Some y; fst (get_cap x s) = {(cap', s)}; cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') x s
 2. \<And>s xa xaa xb xc cap' y. \<lbrakk>pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at (CNode xb xc) xa s; obj_refs capa = {} \<longrightarrow> cap_irqs capa \<noteq> {}; fst x \<noteq> xa; well_formed_cnode_n xb xc; xc xaa = Some y; fst (get_cap x s) = {(cap', s)}; cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> fst x \<noteq> xa
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 7. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 8. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (7 subgoals):
 1. \<And>s xa xaa xb xc cap' y. \<lbrakk>pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at (CNode xb xc) xa s; obj_refs capa = {} \<longrightarrow> cap_irqs capa \<noteq> {}; fst x \<noteq> xa; well_formed_cnode_n xb xc; xc xaa = Some y; fst (get_cap x s) = {(cap', s)}; cap_irqs capa \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs capa \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs capa \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> fst x \<noteq> xa
 2. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 7. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (6 subgoals):
 1. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 2. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (6 subgoals):
 1. \<And>s xa xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, tcb_cnode_index 0); ko_at (TCB xb) xa s; obj_refs capa = {} \<longrightarrow> cap_irqs capa \<noteq> {}; fst x \<noteq> xa\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 2. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 3. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 4. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 5. \<And>s xa xaa ko xb. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {}); fst x \<noteq> fst slot; ko = TCB xb; xaa \<noteq> tcb_cnode_index 0; xaa \<noteq> tcb_cnode_index (Suc 0); xaa \<noteq> tcb_cnode_index 2; xaa \<noteq> tcb_cnode_index 3; xaa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps capa (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)
 6. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa ko. \<lbrakk>x \<in> slots_holding_overlapping_caps capa s; pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag xa; slot = (xa, xaa); ko_at ko xa s; \<not> (obj_refs capa = {} \<and> cap_irqs capa = {})\<rbrakk> \<Longrightarrow> fst x \<noteq> fst slot proof (prove)
goal:
No subgoals!