theory Finalise_AC

lemma rec_del_respects_CTEDelete_transferable':
  "\<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and
    simple_sched_action and emptyable slot and  cdt_change_allowed' aag slot and
    (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrace>
   rec_del (CTEDeleteCall slot exposed)
   \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>,
   \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>" apply (cases "is_subject aag (fst slot)") apply (wp rec_del_respects'') apply (solves \<open>simp\<close>) apply (subst rec_del.simps[abs_def]) apply (wp add: hoare_K_bind without_preemption_wp hoare_weak_lift_imp wp_transferable
                 rec_del_Finalise_transferable
            del: wp_not_transferable
         | wpc)+ apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable) apply simp apply (elim conjE) apply simp apply simp apply (wp add: hoare_K_bind without_preemption_wp hoare_weak_lift_imp wp_transferable
                  rec_del_Finalise_transferable
             del: wp_not_transferable
          | wpc)+ apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable) apply simp apply (elim conjE) apply simp apply simp apply (clarsimp) apply (frule(3) cca_to_transferable_or_subject[OF invs_valid_objs invs_mdb]) by (safe; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall slot exposed) and emptyable (slot_rdcall (CTEDeleteCall slot exposed)) and (\<lambda>s. \<not> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (CTEDeleteCall slot exposed)) s) and K (is_subject aag (fst (slot_rdcall (CTEDeleteCall slot exposed)))) and K (case CTEDeleteCall slot exposed of ReduceZombieCall cap sl x \<Rightarrow> \<forall>x\<in>obj_refs_ac cap. is_subject aag x | _ \<Rightarrow> True)) s \<and> ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall slot exposed) and emptyable (slot_rdcall (CTEDeleteCall slot exposed)) and (\<lambda>s. \<not> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (CTEDeleteCall slot exposed)) s) and K (is_subject aag (fst (slot_rdcall (CTEDeleteCall slot exposed)))) and K (case CTEDeleteCall slot exposed of ReduceZombieCall cap sl x \<Rightarrow> \<forall>x\<in>obj_refs_ac cap. is_subject aag x | _ \<Rightarrow> True)) s
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?P'15\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> True \<and> (if exposed \<or> xa then \<lambda>s. (integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and cdt_change_allowed' aag slot and K (xb = NullCap)) s \<and> (integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and cdt_change_allowed' aag slot and K (xb = NullCap)) s else (\<lambda>s. integrity aag X st s \<and> integrity aag X st s)) s\<rbrace>, \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?P'14\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> ?P'15 s) \<and> ?P'14 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (K (rv = (True, NullCap)) and ?E56) s\<rbrakk> \<Longrightarrow> \<forall>x xa. rv = (x, xa) \<longrightarrow> True \<and> (if exposed \<or> x then \<lambda>s. (integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and cdt_change_allowed' aag slot and K (xa = NullCap)) s \<and> (integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and cdt_change_allowed' aag slot and K (xa = NullCap)) s else (\<lambda>s. integrity aag X st s \<and> integrity aag X st s)) s
 2. \<And>e s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ?E56 s\<rbrakk> \<Longrightarrow> integrity aag X st s
 3. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?P'14\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 4. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and ?E56) s) \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<And>e s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s\<rbrakk> \<Longrightarrow> integrity aag X st s
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?P'14\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<And>e s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; integrity aag X st s; valid_list s; valid_objs s; valid_mdb s; pas_refined aag s; cdt_change_allowed' aag slot s\<rbrakk> \<Longrightarrow> integrity aag X st s
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?P'14\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> ?P'14 s proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?P'14\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> ?P'14 s proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?P'14\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
y <- liftE (when (exposed \<or> success) (empty_slot slot cleanup_info));
returnOk undefined
odE \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> ?P'14 s proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?P'14\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> (trp \<longrightarrow> (if exposed \<or> xa then integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and cdt_change_allowed' aag slot and K (xb = NullCap) else integrity aag X st) s) \<and> (if exposed \<or> xa then pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and is_transferable_in slot else pas_refined aag) s\<rbrace>, \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (K (rv = (True, NullCap)) and ?E102) s\<rbrakk> \<Longrightarrow> \<forall>x xa. rv = (x, xa) \<longrightarrow> (trp \<longrightarrow> (if exposed \<or> x then integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and cdt_change_allowed' aag slot and K (xa = NullCap) else integrity aag X st) s) \<and> (if exposed \<or> x then pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and is_transferable_in slot else pas_refined aag) s
 2. \<And>e s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ?E102 s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> (is_transferable_in slot and ?E102) s proof (prove)
goal (2 subgoals):
 1. \<And>e s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (trp \<longrightarrow> integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s) \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in slot s\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> (is_transferable_in slot and (\<lambda>s. (trp \<longrightarrow> integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s) \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in slot s)) s proof (prove)
goal (2 subgoals):
 1. \<And>e s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; trp \<longrightarrow> integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; is_transferable_in slot s\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> (is_transferable_in slot and (\<lambda>s. (trp \<longrightarrow> integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s) \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in slot s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> (is_transferable_in slot and (\<lambda>s. integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s)) s) \<and> (is_transferable_in slot and (\<lambda>s. (trp \<longrightarrow> integrity aag X st s \<and> valid_list s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> cdt_change_allowed' aag slot s) \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in slot s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (trp \<longrightarrow> integrity aag X st s) \<and> pas_refined aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> cdt_change_allowed' aag slot s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> is_transferable_in slot s \<and> valid_objs s \<and> valid_mdb s) \<and> is_transferable_in slot s \<and> (trp \<longrightarrow> valid_objs s \<and> valid_mdb s) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; trp \<longrightarrow> integrity aag X st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; emptyable slot s; cdt_change_allowed' aag slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> is_transferable_in slot s \<and> valid_objs s \<and> valid_mdb s) \<and> is_transferable_in slot s \<and> (trp \<longrightarrow> valid_objs s \<and> valid_mdb s) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; trp \<longrightarrow> integrity aag X st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; emptyable slot s; cdt_change_allowed' aag slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s; is_subject aag (fst slot) \<or> is_transferable_in slot s\<rbrakk> \<Longrightarrow> (trp \<longrightarrow> is_transferable_in slot s \<and> valid_objs s \<and> valid_mdb s) \<and> is_transferable_in slot s \<and> (trp \<longrightarrow> valid_objs s \<and> valid_mdb s) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in slot s