theory Noninterference

lemma reads_equiv_f_g_affects_equiv_uwr:
  "\<lbrakk> reads_equiv_f_g (current_aag (internal_state_if s))
                     (internal_state_if s') (internal_state_if t');
     affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a)
                   (internal_state_if s') (internal_state_if t');
     (part s, Partition a) \<in> policyFlows (pasPolicy initial_aag); part s \<noteq> PSched;
     silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s');
     (s,t) \<in> uwr PSched;
     partitionIntegrity (current_aag (internal_state_if s))
                        (internal_state_if s) (internal_state_if s');
     partitionIntegrity (current_aag (internal_state_if t))
                        (internal_state_if t) (internal_state_if t');
     sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t' \<rbrakk>
     \<Longrightarrow> (s', t') \<in> uwr (Partition a) \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s)" apply (frule_tac s="internal_state_if s" in partitionIntegrity_cur_domain) apply (subgoal_tac "current_aag (internal_state_if s) = current_aag (internal_state_if s')") apply (case_tac s', case_tac t') apply (case_tac aa, case_tac aaa) apply (rule conjI) apply simp apply (drule (1) reads_g_affects_equiv_sameFor[OF conjI]) apply (simp add: current_aag_def) apply (fastforce) apply (simp add: current_aag_def) apply (rule flow_then_affect) apply (simp add: part_def partition_def split: if_splits) apply (clarsimp simp: uwr_def current_aag_def) apply assumption apply (rule conjI) apply (clarsimp simp: uwr_def sameFor_def sameFor_scheduler_def) apply (clarsimp simp: reads_equiv_f_g_def reads_equiv_def silc_dom_equiv_def current_aag_def
                          globals_equiv_idle_thread_ptr globals_equiv_globals_equiv_scheduler) apply (fastforce simp: domain_fields_equiv_def partitionIntegrity_def) apply (drule sameFor_reads_equiv_f_g) apply (fastforce simp: invs_if_def Invs_def) apply (fastforce simp: current_aag_def) apply (simp add: uwr_def part_def partition_def current_aag_def split: if_splits) apply (simp add: current_aag_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'\<rbrakk> \<Longrightarrow> uwr2 s' (Partition a) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> uwr2 s' (Partition a) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s')\<rbrakk> \<Longrightarrow> uwr2 s' (Partition a) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 2. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba)\<rbrakk> \<Longrightarrow> uwr2 s' (Partition a) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 2. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' (Partition a) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 2. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' (Partition a) t'
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 3. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 ((ac, bb), ba) (Partition a) ((ac, bc), ba)
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 3. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (6 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'10 aa b aaa ba ab bb ac bc) (?st''10 aa b aaa ba ab bb ac bc)
 3. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> Partition a \<in> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 4. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc); (((?uc10 aa b aaa ba ab bb ac bc, bb), ?mode10 aa b aaa ba ab bb ac bc), (?uc10 aa b aaa ba ab bb ac bc, bc), ?mode10 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag bb) (Partition a)\<rbrakk> \<Longrightarrow> uwr2 ((ac, bb), ba) (Partition a) ((ac, bc), ba)
 5. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 6. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (5 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'10 aa b aaa ba ab bb ac bc) (?st''10 aa b aaa ba ab bb ac bc)
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> Partition a \<in> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 3. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc); (((?uc10 aa b aaa ba ab bb ac bc, bb), ?mode10 aa b aaa ba ab bb ac bc), (?uc10 aa b aaa ba ab bb ac bc, bc), ?mode10 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag bb) (Partition a)\<rbrakk> \<Longrightarrow> uwr2 ((ac, bb), ba) (Partition a) ((ac, bc), ba)
 4. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 5. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (4 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> Partition a \<in> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc); (((?uc10 aa b aaa ba ab bb ac bc, bb), ?mode10 aa b aaa ba ab bb ac bc), (?uc10 aa b aaa ba ab bb ac bc, bc), ?mode10 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag bb) (Partition a)\<rbrakk> \<Longrightarrow> uwr2 ((ac, bb), ba) (Partition a) ((ac, bc), ba)
 3. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 4. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (4 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bb))\<rparr>) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bb))\<rparr>) s0_internal bb; uwr2 s PSched t; partitionIntegrity (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bb))\<rparr>) (internal_state_if s) bb; partitionIntegrity (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))\<rparr>) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> Partition a \<in> partsSubjectAffects (pasPolicy initial_aag) (label_of (the_elem (pasDomainAbs initial_aag (cur_domain bb))))
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc); (((?uc10 aa b aaa ba ab bb ac bc, bb), ?mode10 aa b aaa ba ab bb ac bc), (?uc10 aa b aaa ba ab bb ac bc, bc), ?mode10 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag bb) (Partition a)\<rbrakk> \<Longrightarrow> uwr2 ((ac, bb), ba) (Partition a) ((ac, bc), ba)
 3. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 4. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (4 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bb))\<rparr>) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bb))\<rparr>) s0_internal bb; uwr2 s PSched t; partitionIntegrity (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bb))\<rparr>) (internal_state_if s) bb; partitionIntegrity (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))\<rparr>) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> policy2 (Partition (label_of (the_elem (pasDomainAbs initial_aag (cur_domain bb))))) (Partition a)
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc); (((?uc10 aa b aaa ba ab bb ac bc, bb), ?mode10 aa b aaa ba ab bb ac bc), (?uc10 aa b aaa ba ab bb ac bc, bc), ?mode10 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag bb) (Partition a)\<rbrakk> \<Longrightarrow> uwr2 ((ac, bb), ba) (Partition a) ((ac, bc), ba)
 3. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 4. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag bb) (OrdinaryLabel a) bb bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag bb) s0_internal bb; uwr2 s PSched t; partitionIntegrity (current_aag bb) (internal_state_if s) bb; partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) bc; b = ba; ab = ac; cur_domain (internal_state_if s) = cur_domain bb; current_aag (internal_state_if s) = current_aag bb; s' = ((ac, bb), ba); t' = ((ac, bc), ba); aa = (ac, bb); aaa = (ac, bc); (((?uc10 aa b aaa ba ab bb ac bc, bb), ?mode10 aa b aaa ba ab bb ac bc), (?uc10 aa b aaa ba ab bb ac bc, bc), ?mode10 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag bb) (Partition a)\<rbrakk> \<Longrightarrow> uwr2 ((ac, bb), ba) (Partition a) ((ac, bc), ba)
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 3. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<And>baa bba ac bc. \<lbrakk>affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bba))\<rparr>) (OrdinaryLabel a) bba bc; policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bba))\<rparr>) s0_internal bba; (s, t) \<in> same_for initial_aag PSched; partitionIntegrity (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bba))\<rparr>) (internal_state_if s) bba; partitionIntegrity (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))\<rparr>) (internal_state_if t) bc; cur_domain (internal_state_if s) = cur_domain bba; s' = ((ac, bba), baa); t' = ((ac, bc), baa); (((?uc10 (ac, bba) baa (ac, bc) baa ac bba ac bc, bba), ?mode10 (ac, bba) baa (ac, bc) baa ac bba ac bc), (?uc10 (ac, bba) baa (ac, bc) baa ac bba ac bc, bc), ?mode10 (ac, bba) baa (ac, bc) baa ac bba ac bc) \<in> same_for initial_aag (Partition a)\<rbrakk> \<Longrightarrow> (((ac, bba), baa), (ac, bc), baa) \<in> same_for initial_aag (Partition a)
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 3. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
 2. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' PSched t'
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' (part s) t'
 3. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<And>baa bba ac bc ad bd be ae bf bg. \<lbrakk>reads_equiv_f_g (current_aag bba) bba bc; affects_equiv (current_aag bba) (OrdinaryLabel a) bba bc; policy2 (part ((ad, bd), be)) (Partition a); part ((ad, bd), be) \<noteq> PSched; silc_inv (current_aag bba) s0_internal bba; partitionIntegrity (current_aag bba) bd bba; partitionIntegrity (current_aag bf) bf bc; cur_domain bd = cur_domain bba; current_aag bd = current_aag bba; s' = ((ac, bba), baa); t' = ((ac, bc), baa); s = ((ad, bd), be); t = ((ae, bf), bg); domain_fields_equiv bd bf; idle_thread bd = idle_thread bf; globals_equiv_scheduler bd bf; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap bd bf; equiv_irq_state (machine_state bd) (machine_state bf); scheduler_modes be = scheduler_modes bg; interrupted_modes be = interrupted_modes bg\<rbrakk> \<Longrightarrow> domain_fields_equiv bba bc \<and> idle_thread bba = idle_thread bc \<and> globals_equiv_scheduler bba bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap bba bc \<and> equiv_irq_state (machine_state bba) (machine_state bc)
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' (part s) t'
 3. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<And>baa bba ac bc ad bd be ae bf bg. \<lbrakk>affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bc))\<rparr>) (OrdinaryLabel a) bba bc; policy2 (part ((ad, bd), be)) (Partition a); part ((ad, bd), be) \<noteq> PSched; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bc))\<rparr>) s0_internal bba; partitionIntegrity (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bc))\<rparr>) bd bba; partitionIntegrity (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bf))\<rparr>) bf bc; cur_domain bd = cur_domain bc; s' = ((ac, bba), baa); t' = ((ac, bc), baa); s = ((ad, bd), be); t = ((ae, bf), bg); domain_fields_equiv bd bf; idle_thread bd = idle_thread bf; globals_equiv_scheduler bd bf; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap bd bf; equiv_irq_state (machine_state bd) (machine_state bf); scheduler_modes be = scheduler_modes bg; interrupted_modes be = interrupted_modes bg; \<forall>d\<in>subjectReads (pasPolicy initial_aag) (the_elem (pasDomainAbs initial_aag (cur_domain bc))). states_equiv_for (\<lambda>x. d = pasObjectAbs initial_aag x) (\<lambda>x. d = pasIRQAbs initial_aag x) (\<lambda>x. d = pasASIDAbs initial_aag x) (\<lambda>x. d \<in> pasDomainAbs initial_aag x) bba bc; cur_thread bba = cur_thread bc; cur_domain bba = cur_domain bc; scheduler_action bba = scheduler_action bc; work_units_completed bba = work_units_completed bc; equiv_irq_state (machine_state bba) (machine_state bc); globals_equiv bba bc; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap bba bc\<rbrakk> \<Longrightarrow> domain_fields_equiv bba bc
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' (part s) t'
 3. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> uwr2 s' (part s) t'
 2. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (4 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s)) (?st'101 aa b aaa ba ab bb ac bc) (?st''101 aa b aaa ba ab bb ac bc)
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> pasSubject (current_aag (internal_state_if s)) \<in> pasDomainAbs (current_aag (internal_state_if s)) (cur_domain (internal_state_if s')) \<union> pasDomainAbs (current_aag (internal_state_if s)) (cur_domain (internal_state_if t'))
 3. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc); (((?uc101 aa b aaa ba ab bb ac bc, internal_state_if s'), ?mode101 aa b aaa ba ab bb ac bc), (?uc101 aa b aaa ba ab bb ac bc, internal_state_if t'), ?mode101 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag (internal_state_if s)) (Partition (label_of (pasSubject (current_aag (internal_state_if s)))))\<rbrakk> \<Longrightarrow> uwr2 s' (part s) t'
 4. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (3 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc)\<rbrakk> \<Longrightarrow> pasSubject (current_aag (internal_state_if s)) \<in> pasDomainAbs (current_aag (internal_state_if s)) (cur_domain (internal_state_if s')) \<union> pasDomainAbs (current_aag (internal_state_if s)) (cur_domain (internal_state_if t'))
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc); (((?uc101 aa b aaa ba ab bb ac bc, internal_state_if s'), ?mode101 aa b aaa ba ab bb ac bc), (?uc101 aa b aaa ba ab bb ac bc, internal_state_if t'), ?mode101 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag (internal_state_if s)) (Partition (label_of (pasSubject (current_aag (internal_state_if s)))))\<rbrakk> \<Longrightarrow> uwr2 s' (part s) t'
 3. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s'); current_aag (internal_state_if s) = current_aag (internal_state_if s'); s' = (aa, b); t' = (aaa, ba); aa = (ab, bb); aaa = (ac, bc); (((?uc101 aa b aaa ba ab bb ac bc, internal_state_if s'), ?mode101 aa b aaa ba ab bb ac bc), (?uc101 aa b aaa ba ab bb ac bc, internal_state_if t'), ?mode101 aa b aaa ba ab bb ac bc) \<in> same_for (current_aag (internal_state_if s)) (Partition (label_of (pasSubject (current_aag (internal_state_if s)))))\<rbrakk> \<Longrightarrow> uwr2 s' (part s) t'
 2. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s') (internal_state_if t'); affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel a) (internal_state_if s') (internal_state_if t'); policy2 (part s) (Partition a); part s \<noteq> PSched; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); uwr2 s PSched t; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); partitionIntegrity (current_aag (internal_state_if t)) (internal_state_if t) (internal_state_if t'); sys_mode_of s' = sys_mode_of t'; user_context_of s' = user_context_of t'; cur_domain (internal_state_if s) = cur_domain (internal_state_if s')\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s) = current_aag (internal_state_if s') proof (prove)
goal:
No subgoals!