theory Noninterference

lemma partitionIntegrity_subjectAffects_cdt_list:
  "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s';
     valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s';
     pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x,y) \<noteq> cdt_list s' (x,y) \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag x \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" apply (drule partitionIntegrity_integrity) apply (drule integrity_subjects_cdt_list) apply (simp add: integrity_cdt_list_def) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (elim disjE) apply (drule(1) neq_filtered_ex) apply (elim bexE) apply (case_tac "pasObjectAbs aag x = SilcLabel") apply (subgoal_tac "pasObjectAbs aag (fst xa) = SilcLabel") apply simp apply (rule affects_delete_derived) apply (frule (3) cdt_change_allowed_delete_derived[OF invs_valid_objs invs_mdb]) apply force subgoal by (fastforce simp add: silc_inv_def valid_list_2_def all_children_def
                          simp del: split_paired_All) apply (rule affects_delete_derived2) apply (frule (3) cdt_change_allowed_delete_derived[OF invs_valid_objs invs_mdb]) apply assumption subgoal by (fastforce dest!: aag_cdt_link_DeleteDerived
                         simp add: valid_list_2_def
                         simp del: split_paired_All) apply (rule affects_delete_derived) apply (frule(3) cdt_change_allowed_delete_derived[OF invs_valid_objs invs_mdb]) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); \<forall>x. cdt_list_integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s' x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); \<forall>a b. filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (a, b)) (cdt_list s' (a, b)) \<or> cdt_change_allowed' aag (a, b) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); \<forall>b. filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, b)) (cdt_list s' (x, b)) \<or> cdt_change_allowed' aag (x, b) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)) \<or> cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); \<exists>x\<in>set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)). cdt_change_allowed' aag x s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel; pasObjectAbs aag (fst xa) = SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst xa) = SilcLabel
 3. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<or> xa \<in> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel; pasObjectAbs aag (fst xa) = SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag SilcLabel
 2. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst xa) = SilcLabel
 3. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<or> xa \<in> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel; pasObjectAbs aag (fst xa) = SilcLabel\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, SilcLabel) \<in> pasPolicy aag
 2. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst xa) = SilcLabel
 3. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<or> xa \<in> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel; pasObjectAbs aag (fst xa) = SilcLabel; (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst xa)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, SilcLabel) \<in> pasPolicy aag
 2. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst xa) = SilcLabel
 3. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst xa) = SilcLabel
 2. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa_ \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa_ s; pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst xa_) = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, ?l'24 xa) \<in> pasPolicy aag
 2. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, DeleteDerived, ?l'24 xa) \<in> pasPolicy aag
 3. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel; (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst xa)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, ?l'24 xa) \<in> pasPolicy aag
 2. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, DeleteDerived, ?l'24 xa) \<in> pasPolicy aag
 3. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, DeleteDerived, pasObjectAbs aag (fst xa)) \<in> pasPolicy aag
 2. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt s) (tcb_states_of_state s)) (cdt_list s (x, y)) (cdt_list s' (x, y)); xa_ \<in> set (cdt_list s (x, y)) \<union> set (cdt_list s' (x, y)); cdt_change_allowed' aag xa_ s; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, DeleteDerived, pasObjectAbs aag (fst xa_)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; valid_list s; valid_list s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; invs s; invs s'; cdt_list s (x, y) \<noteq> cdt_list s' (x, y); cdt_change_allowed' aag (x, y) s; (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst (x, y))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag