theory Access_AC

lemma integrity_mono:
  "\<lbrakk> integrity_subjects S aag activate X s s'; S \<subseteq> T; pas_refined aag s; valid_objs s \<rbrakk>
     \<Longrightarrow> integrity_subjects T aag activate X s s'" apply (clarsimp simp: integrity_subjects_def simp del: split_paired_All) apply (rule conjI) apply clarsimp apply (drule_tac x=x in spec)+ apply (simp only: integrity_obj_def) apply (erule rtranclp_monoE) apply (erule integrity_obj_atomic.cases[OF _ integrity_obj_atomic.intros];
          auto simp: indirect_send_def direct_send_def direct_call_def direct_reply_def
               elim: reply_cap_deletion_integrity_mono cnode_integrity_mono
                     arch_integrity_obj_atomic_mono)[1] apply (rule conjI) apply clarsimp apply (drule_tac x=x in spec)+ apply (erule integrity_eobj.cases; auto intro: integrity_eobj.intros) apply (rule conjI) apply (intro allI) apply (drule_tac x=x in spec)+ apply (erule integrity_cdtE; auto elim: cdt_change_allowed_mono) apply (rule conjI) apply (intro allI) apply (drule_tac x=x in spec)+ apply (erule integrity_cdt_listE;
          auto elim!: weaken_filter_eq' intro: integrity_cdt_list_intros
               elim: cdt_change_allowed_mono) apply (rule conjI) apply (fastforce simp: integrity_interrupts_def) apply (rule conjI) apply (clarsimp simp: integrity_ready_queues_def) apply blast apply (rule conjI) apply clarsimp apply (drule_tac x=x in spec, erule integrity_mem.cases;
          blast intro: integrity_mem.intros trm_ipc') apply (rule conjI) apply clarsimp apply (drule_tac x=x in spec, erule integrity_device.cases;
          blast intro: integrity_device.intros) apply (fastforce elim: integrity_asids_mono) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_subjects S aag activate X s s'; S \<subseteq> T; pas_refined aag s; valid_objs s\<rbrakk> \<Longrightarrow> integrity_subjects T aag activate X s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_obj_state aag activate T s s' \<and> (\<forall>x. integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_obj_state aag activate T s s'
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>a b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt s (a, b), is_original_cap s (a, b)) (cdt s' (a, b), is_original_cap s' (a, b)); \<forall>a b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt_list s (a, b)) (cdt_list s' (a, b)); \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_obj aag activate T (pasObjectAbs aag x) (kheap s x) (kheap s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); integrity_obj aag activate S (pasObjectAbs aag x) (kheap s x) (kheap s' x); integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (x, b) (cdt s (x, b), is_original_cap s (x, b)) (cdt s' (x, b), is_original_cap s' (x, b)); \<forall>b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (x, b) (cdt_list s (x, b)) (cdt_list s' (x, b)); integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); integrity_asids aag S x x s s'\<rbrakk> \<Longrightarrow> integrity_obj aag activate T (pasObjectAbs aag x) (kheap s x) (kheap s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); (integrity_obj_atomic aag activate S (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s' x); integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (x, b) (cdt s (x, b), is_original_cap s (x, b)) (cdt s' (x, b), is_original_cap s' (x, b)); \<forall>b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (x, b) (cdt_list s (x, b)) (cdt_list s' (x, b)); integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); integrity_asids aag S x x s s'\<rbrakk> \<Longrightarrow> (integrity_obj_atomic aag activate T (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x xa y. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (x, b) (cdt s (x, b), is_original_cap s (x, b)) (cdt s' (x, b), is_original_cap s' (x, b)); \<forall>b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (x, b) (cdt_list s (x, b)) (cdt_list s' (x, b)); integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); integrity_asids aag S x x s s'; integrity_obj_atomic aag activate S (pasObjectAbs aag x) xa y\<rbrakk> \<Longrightarrow> integrity_obj_atomic aag activate T (pasObjectAbs aag x) xa y
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> \<forall>x. integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>a b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt s (a, b), is_original_cap s (a, b)) (cdt s' (a, b), is_original_cap s' (a, b)); \<forall>a b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt_list s (a, b)) (cdt_list s' (a, b)); \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); integrity_obj aag activate S (pasObjectAbs aag x) (kheap s x) (kheap s' x); integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (x, b) (cdt s (x, b), is_original_cap s (x, b)) (cdt s' (x, b), is_original_cap s' (x, b)); \<forall>b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (x, b) (cdt_list s (x, b)) (cdt_list s' (x, b)); integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); integrity_asids aag S x x s s'\<rbrakk> \<Longrightarrow> integrity_eobj aag T (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_state aag T s s' \<and> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_state aag T s s'
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt aag T (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s' x, is_original_cap s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'; integrity_cdt aag S (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s' x, is_original_cap s' x); integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s' x)\<rbrakk> \<Longrightarrow> integrity_cdt aag T (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s' x, is_original_cap s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_list_state aag T s s' \<and> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_list_state aag T s s'
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_cdt_list aag T (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'; integrity_cdt aag S (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s' x, is_original_cap s' x); integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s' x)\<rbrakk> \<Longrightarrow> integrity_cdt_list aag T (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> \<forall>x. integrity_interrupts aag T x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> \<forall>d p. integrity_ready_queues aag T (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>d p. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>a b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt s (a, b), is_original_cap s (a, b)) (cdt s' (a, b), is_original_cap s' (a, b)); \<forall>a b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt_list s (a, b)) (cdt_list s' (a, b)); \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d. pasDomainAbs aag d \<inter> S = {} \<longrightarrow> (\<forall>p. \<exists>threads. threads @ ready_queues s d p = ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'; pasDomainAbs aag d \<inter> T = {}; \<not> pasMayEditReadyQueues aag\<rbrakk> \<Longrightarrow> \<exists>threads. threads @ ready_queues s d p = ready_queues s' d p
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> \<forall>x. integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>a b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt s (a, b), is_original_cap s (a, b)) (cdt s' (a, b), is_original_cap s' (a, b)); \<forall>a b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt_list s (a, b)) (cdt_list s' (a, b)); \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_mem aag T x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag T x a s s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> \<forall>x. integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag T x a s s' proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>a b. integrity_cdt aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt s (a, b), is_original_cap s (a, b)) (cdt s' (a, b), is_original_cap s' (a, b)); \<forall>a b. integrity_cdt_list aag S (cdt s) (tcb_states_of_state s) (a, b) (cdt_list s (a, b)) (cdt_list s' (a, b)); \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> integrity_device aag T x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)
 2. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag T x a s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; pas_refined aag s; valid_objs s; integrity_obj_state aag activate S s s'; \<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); integrity_cdt_state aag S s s'; integrity_cdt_list_state aag S s s'; \<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag S x a s s'\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag T x a s s' proof (prove)
goal:
No subgoals!