theory CNode_AC

lemma cap_swap_respects[wp]:
  "\<lbrace>integrity aag X st and pas_refined aag
                       and K (is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace>
   cap_swap cap slot cap' slot'
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: cap_swap_def) apply (wp get_cap_wp set_cap_integrity_autarch cap_swap_list_integrity
            cap_swap_ext_extended_list_integ_lift[where Q="\<top>"]
            set_original_integrity_autarch[unfolded pred_conj_def K_def]
         | simp add: set_cdt_def split del: if_split | blast)+ apply (rule wp_integrity_clean') apply (simp add: integrity_def) apply (blast intro: cca_owned) apply (wpsimp wp: set_cap_integrity_autarch set_cap_pas_refined)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace> cap_swap cap slot cap' slot' \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<and> is_subject aag (fst slot') \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag\<rbrace> cap_swap cap slot cap' slot' \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag\<rbrace> do y <- set_cap cap' slot;
y <- set_cap cap slot';
slot1_p <- gets (\<lambda>s. cdt s slot);
slot2_p <- gets (\<lambda>s. cdt s slot');
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some slot then Some slot' else if cdt n = Some slot' then Some slot else cdt n)(slot := if cdt slot' = Some slot then Some slot' else if cdt slot' = Some slot' then Some slot else cdt slot', slot' := if cdt slot = Some slot then Some slot' else if cdt slot = Some slot' then Some slot else cdt slot));
y <- cap_swap_ext slot slot' slot1_p slot2_p;
is_original <- gets is_original_cap;
y <- set_original slot (is_original slot');
set_original slot' (is_original slot)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>?B4 ()\<rbrace> set_cap cap slot' \<lbrace>\<lambda>ya s. integrity aag X st (s\<lparr>cdt := \<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a\<rparr>)\<rbrace>
 2. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>?Q3\<rbrace> set_cap cap' slot \<lbrace>?B4\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot'); (integrity aag X st and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>cdt := \<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a\<rparr>)
 2. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>?B4 ()\<rbrace> set_cap cap slot' \<lbrace>\<lambda>ya. integrity aag X st\<rbrace>
 3. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>?Q3\<rbrace> set_cap cap' slot \<lbrace>?B4\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot'); (integrity aag X st and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> (cdt s slot' = Some slot' \<longrightarrow> slot' \<noteq> slot \<longrightarrow> (cdt s slot = Some slot' \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot', is_original_cap s slot) (Some slot, is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot', is_original_cap s slot') (Some slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> (cdt s (a, b) = Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot', is_original_cap s slot) (Some slot, is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot', is_original_cap s slot') (Some slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot', is_original_cap s slot) (Some slot, is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> (a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot', is_original_cap s slot') (Some slot, is_original_cap s slot')))))) \<and> (cdt s slot \<noteq> Some slot' \<longrightarrow> (cdt s slot = Some slot \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> (a, b) \<noteq> slot \<longrightarrow> (a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> cdt s (a, b) = Some slot \<longrightarrow> (a, b) \<noteq> slot \<longrightarrow> (a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s slot \<noteq> Some slot \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (Some slot, is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot', is_original_cap s slot') (cdt s slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> (cdt s (a, b) = Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (Some slot, is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot', is_original_cap s slot') (cdt s slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (Some slot, is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> (a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot', is_original_cap s slot') (cdt s slot, is_original_cap s slot')))))))) \<and> (cdt s slot' \<noteq> Some slot' \<longrightarrow> (cdt s slot' = Some slot \<longrightarrow> (cdt s slot = Some slot' \<longrightarrow> slot' \<noteq> slot \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> (a, b) \<noteq> slot \<longrightarrow> (a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> cdt s (a, b) = Some slot \<longrightarrow> (a, b) \<noteq> slot \<longrightarrow> (a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s slot \<noteq> Some slot' \<longrightarrow> (cdt s slot = Some slot \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> slot' \<noteq> slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot, is_original_cap s slot) (Some slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot, is_original_cap s slot') (Some slot', is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> (cdt s (a, b) = Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> slot \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot, is_original_cap s slot) (Some slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot, is_original_cap s slot') (Some slot', is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> slot \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot, is_original_cap s slot) (Some slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> (a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot, is_original_cap s slot') (Some slot', is_original_cap s slot')))))) \<and> (cdt s slot \<noteq> Some slot \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> slot' \<noteq> slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (Some slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot, is_original_cap s slot') (cdt s slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> (cdt s (a, b) = Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> slot \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (Some slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot, is_original_cap s slot') (cdt s slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> slot \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (Some slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> (a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (Some slot, is_original_cap s slot') (cdt s slot, is_original_cap s slot')))))))) \<and> (cdt s slot' \<noteq> Some slot \<longrightarrow> (cdt s slot = Some slot' \<longrightarrow> slot' \<noteq> slot \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot', is_original_cap s slot) (cdt s slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (Some slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> (cdt s (a, b) = Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot', is_original_cap s slot) (cdt s slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (Some slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot', is_original_cap s slot) (cdt s slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> (a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (Some slot, is_original_cap s slot')))))) \<and> (cdt s slot \<noteq> Some slot' \<longrightarrow> (cdt s slot = Some slot \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> slot' \<noteq> slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot, is_original_cap s slot) (cdt s slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (Some slot', is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> (cdt s (a, b) = Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> (slot = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (Some slot', is_original_cap s slot')) \<and> (slot \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot, is_original_cap s slot) (cdt s slot', is_original_cap s slot))) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (Some slot', is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> (slot = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (Some slot', is_original_cap s slot')) \<and> (slot \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (Some slot, is_original_cap s slot) (cdt s slot', is_original_cap s slot))) \<and> ((a, b) \<noteq> slot \<longrightarrow> (a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (Some slot', is_original_cap s slot')))))) \<and> (cdt s slot \<noteq> Some slot \<longrightarrow> (\<forall>a b. (cdt s (a, b) = Some slot' \<longrightarrow> slot' \<noteq> slot \<longrightarrow> ((a, b) = slot \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (cdt s slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (cdt s slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot', is_original_cap s (a, b)) (Some slot, is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot' \<longrightarrow> (cdt s (a, b) = Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> slot \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (cdt s slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> ((a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (cdt s slot, is_original_cap s slot')) \<and> ((a, b) \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) (a, b) (Some slot, is_original_cap s (a, b)) (Some slot', is_original_cap s (a, b))))) \<and> (cdt s (a, b) \<noteq> Some slot \<longrightarrow> ((a, b) = slot \<longrightarrow> slot \<noteq> slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot (cdt s slot, is_original_cap s slot) (cdt s slot', is_original_cap s slot)) \<and> ((a, b) \<noteq> slot \<longrightarrow> (a, b) = slot' \<longrightarrow> cdt_integrity aag (cdt s) (tcb_states_of_state s) slot' (cdt s slot', is_original_cap s slot') (cdt s slot, is_original_cap s slot')))))))))
 2. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>?B4 ()\<rbrace> set_cap cap slot' \<lbrace>\<lambda>ya. integrity aag X st\<rbrace>
 3. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>?Q3\<rbrace> set_cap cap' slot \<lbrace>?B4\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot'); (integrity aag X st and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>?B4 ()\<rbrace> set_cap cap slot' \<lbrace>\<lambda>ya. integrity aag X st\<rbrace>
 2. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot')\<rbrakk> \<Longrightarrow> \<lbrace>?Q3\<rbrace> set_cap cap' slot \<lbrace>?B4\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag (fst slot); is_subject aag (fst slot'); (integrity aag X st and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal:
No subgoals!