theory Noninterference

lemma partitionIntegrity_subjectAffects_ready_queues:
  assumes domains_distinct: "pas_domains_distinct (aag :: 'a subject_label PAS)"
  shows "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; einvs s; einvs s';
           pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag;
           silc_inv aag st s; silc_inv aag st' s'; ready_queues s d \<noteq> ready_queues s' d;
           cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s);
           cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s') \<rbrakk>
           \<Longrightarrow> pasDomainAbs aag d \<inter> subjectAffects (pasPolicy aag) (pasSubject aag) \<noteq> {}" apply (clarsimp simp: disjoint_iff_not_equal) apply (frule valid_sched_valid_blocked[where s=s]) apply (case_tac "pasSubject aag \<in> pasDomainAbs aag d") apply (metis affects_lrefl) apply (drule fun_noteqD,clarsimp) apply (clarsimp simp add: partitionIntegrity_def) apply (frule_tac d=d and p=a in integrity_subjects_ready_queues[rule_format]) apply (clarsimp simp: integrity_ready_queues_def) apply (case_tac "threads = []") apply simp apply (erule not_NilE) apply (frule_tac x=x and d=d and p=a and s=s' in tcb_with_domain_at[OF valid_sched_valid_queues]) apply (drule_tac t="ready_queues s' d a" in sym) apply simp apply clarsimp apply (frule(1) tcb_domain_wellformed) apply (rename_tac tcb_ptr tcbs tcb) apply (rule_tac x = "pasObjectAbs aag tcb_ptr" in bexI) apply (case_tac "scheduler_action s = switch_thread tcb_ptr") apply (drule switch_to_cur_domain[rotated]) apply simp apply simp apply (fastforce dest: domains_distinct[THEN pas_domains_distinct_inj]) apply (case_tac "ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr") apply (rule_tac s=s and s'=s' in partitionIntegrity_subjectAffects_eobj) apply (simp add: partitionIntegrity_def)+ apply (subgoal_tac "kheap s tcb_ptr \<noteq> kheap s' tcb_ptr") apply (rule partitionIntegrity_subjectAffects_obj) apply (fastforce simp add: partitionIntegrity_def valid_sched_def)+ apply (rule_tac threads="tcb_ptr # tcbs" in ready_queues_alters_kheap) apply (fastforce simp add: partitionIntegrity_def valid_sched_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; einvs s; einvs s'; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ready_queues s d \<noteq> ready_queues s' d; cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s')\<rbrakk> \<Longrightarrow> pasDomainAbs aag d \<inter> subjectAffects (pasPolicy aag) (pasSubject aag) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ready_queues s d \<noteq> ready_queues s' d; cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ready_queues s d \<noteq> ready_queues s' d; cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; valid_blocked s\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ready_queues s d \<noteq> ready_queues s' d; cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x
 2. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ready_queues s d \<noteq> ready_queues s' d; cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; ready_queues s d \<noteq> ready_queues s' d; cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; integrity_ready_queues (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasDomainAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) d) (ready_queues s d a) (ready_queues s' d a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a threads. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (2 subgoals):
 1. \<And>a threads. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a; threads = []\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x
 2. \<And>a threads. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a; threads \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a threads. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a; threads \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a threads x xs'. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a; threads = x # xs'\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (2 subgoals):
 1. \<And>a threads x xs'. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a; threads = x # xs'\<rbrakk> \<Longrightarrow> x \<in> set (ready_queues s' d a)
 2. \<And>a threads x xs'. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a; threads = x # xs'; \<exists>t. ekheap s' x = Some t \<and> tcb_domain t = d\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (2 subgoals):
 1. \<And>a threads x xs'. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads = x # xs'; ready_queues s' d a = threads @ ready_queues s d a\<rbrakk> \<Longrightarrow> x \<in> set (ready_queues s' d a)
 2. \<And>a threads x xs'. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a; threads = x # xs'; \<exists>t. ekheap s' x = Some t \<and> tcb_domain t = d\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a threads x xs'. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag d; ready_queues s d a \<noteq> ready_queues s' d a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; threads @ ready_queues s d a = ready_queues s' d a; threads = x # xs'; \<exists>t. ekheap s' x = Some t \<and> tcb_domain t = d\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag d. subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a x xs' t. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain t); ready_queues s (tcb_domain t) a \<noteq> ready_queues s' (tcb_domain t) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; x # xs' @ ready_queues s (tcb_domain t) a = ready_queues s' (tcb_domain t) a; ekheap s' x = Some t; d = tcb_domain t\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag (tcb_domain t). subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a x xs' t. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain t); ready_queues s (tcb_domain t) a \<noteq> ready_queues s' (tcb_domain t) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; x # xs' @ ready_queues s (tcb_domain t) a = ready_queues s' (tcb_domain t) a; ekheap s' x = Some t; d = tcb_domain t; pasObjectAbs aag x \<in> pasDomainAbs aag (tcb_domain t)\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag (tcb_domain t). subject_can_affect_label_directly aag x proof (prove)
goal (1 subgoal):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>pasDomainAbs aag (tcb_domain tcb). subject_can_affect_label_directly aag x proof (prove)
goal (2 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (3 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s = switch_thread tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (5 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pas_refined (?aag51 a tcb_ptr tcbs tcb) s
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> valid_sched s
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); pasObjectAbs (?aag51 a tcb_ptr tcbs tcb) tcb_ptr \<in> pasDomainAbs (?aag51 a tcb_ptr tcbs tcb) (cur_domain s)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 4. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 5. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (4 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> valid_sched s
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (cur_domain s)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 4. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (3 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (cur_domain s)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (2 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (3 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; \<not> ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (11 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> partitionIntegrity aag s s'
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> valid_objs s
 4. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> einvs s
 5. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> einvs s'
 6. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference aag
 7. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> silc_inv aag (?st71 a tcb_ptr tcbs tcb) s
 8. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> silc_inv aag (?st'71 a tcb_ptr tcbs tcb) s'
 9. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr
 10. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; \<not> ekheap s tcb_ptr \<noteq> ekheap s' tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
A total of 11 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (3 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb; kheap s tcb_ptr \<noteq> kheap s' tcb_ptr\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag tcb_ptr)
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> kheap s tcb_ptr \<noteq> kheap s' tcb_ptr
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (8 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb; kheap s tcb_ptr \<noteq> kheap s' tcb_ptr\<rbrakk> \<Longrightarrow> partitionIntegrity aag (?s73 a tcb_ptr tcbs tcb) (?s'73 a tcb_ptr tcbs tcb)
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb; kheap s tcb_ptr \<noteq> kheap s' tcb_ptr\<rbrakk> \<Longrightarrow> pas_refined aag (?s73 a tcb_ptr tcbs tcb)
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb; kheap s tcb_ptr \<noteq> kheap s' tcb_ptr\<rbrakk> \<Longrightarrow> invs (?s73 a tcb_ptr tcbs tcb)
 4. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb; kheap s tcb_ptr \<noteq> kheap s' tcb_ptr\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference aag
 5. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb; kheap s tcb_ptr \<noteq> kheap s' tcb_ptr\<rbrakk> \<Longrightarrow> silc_inv aag (?st73 a tcb_ptr tcbs tcb) (?s73 a tcb_ptr tcbs tcb)
 6. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb; kheap s tcb_ptr \<noteq> kheap s' tcb_ptr\<rbrakk> \<Longrightarrow> kheap (?s73 a tcb_ptr tcbs tcb) tcb_ptr \<noteq> kheap (?s'73 a tcb_ptr tcbs tcb) tcb_ptr
 7. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> kheap s tcb_ptr \<noteq> kheap s' tcb_ptr
 8. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (2 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> kheap s tcb_ptr \<noteq> kheap s' tcb_ptr
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb) proof (prove)
goal (14 subgoals):
 1. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> valid_queues s
 2. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> valid_blocked s
 3. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> valid_idle s'
 4. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> ready_queues s (?d146 a tcb_ptr tcbs tcb) (?a146 a tcb_ptr tcbs tcb) \<noteq> ready_queues s' (?d146 a tcb_ptr tcbs tcb) (?a146 a tcb_ptr tcbs tcb)
 5. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> (tcb_ptr # tcbs) @ ready_queues s (?d146 a tcb_ptr tcbs tcb) (?a146 a tcb_ptr tcbs tcb) = ready_queues s' (?d146 a tcb_ptr tcbs tcb) (?a146 a tcb_ptr tcbs tcb)
 6. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> valid_queues s'
 7. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> valid_etcbs s
 8. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> valid_etcbs s'
 9. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> tcb_ptr \<in> set (tcb_ptr # tcbs)
 10. \<And>a tcb_ptr tcbs tcb. \<lbrakk>pas_refined aag s; valid_objs s; pas_refined aag s'; pas_cur_domain aag s; pas_wellformed_noninterference aag; silc_inv aag st s; silc_inv aag st' s'; cur_thread s \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s); cur_thread s' \<noteq> idle_thread s' \<longrightarrow> is_subject aag (cur_thread s'); invs s; invs s'; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s'); valid_list s'; valid_sched s'; valid_blocked s; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain tcb); ready_queues s (tcb_domain tcb) a \<noteq> ready_queues s' (tcb_domain tcb) a; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s s'; domain_fields_equiv s s'; idle_thread s = idle_thread s'; globals_equiv_scheduler s s'; silc_dom_equiv aag s s'; tcb_ptr # tcbs @ ready_queues s (tcb_domain tcb) a = ready_queues s' (tcb_domain tcb) a; ekheap s' tcb_ptr = Some tcb; d = tcb_domain tcb; pasObjectAbs aag tcb_ptr \<in> pasDomainAbs aag (tcb_domain tcb); scheduler_action s \<noteq> switch_thread tcb_ptr; ekheap s tcb_ptr = Some tcb\<rbrakk> \<Longrightarrow> ekheap s tcb_ptr = ekheap s' tcb_ptr
A total of 14 subgoals... proof (prove)
goal:
No subgoals!