theory Noninterference

lemma integrity_part:
  "\<lbrakk> system.reachable (big_step_ADT_A_if utf) s0 s;
     (s, s') \<in> Simulation.Step (big_step_ADT_A_if utf) ();
     (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> (s,s') \<in> uwr u" supply [[simp_depth_limit=0]] \<comment> \<open>speedup\<close> apply (simp add: uwr_def_cur[where s=s]) apply (case_tac s, case_tac s', simp) apply (case_tac a, case_tac aa, simp) apply (rule partsSubjectAffects_bounds_subjects_affects) apply (rule current_domains_distinct) apply (fastforce dest: Step_partitionIntegrity) apply (fastforce dest: pas_refined_initial_aag_reachable simp: pas_refined_cur) apply (frule (2) pas_refined_current_aag'[OF _ Step_current_aag_unchanged[symmetric],
                                                        OF reachable_Step']; force) apply (fastforce dest!: reachable_invs_if simp: invs_if_def Invs_def) apply (fastforce dest!: reachable_invs_if[OF reachable_Step'] simp: invs_if_def Invs_def) apply (fastforce dest!: reachable_invs_if simp: invs_if_def Invs_def) apply (fastforce dest!: reachable_invs_if[OF reachable_Step'] simp: invs_if_def Invs_def) apply (fastforce dest: silc_inv_initial_aag_reachable simp: silc_inv_cur) apply (frule Step_current_aag_unchanged[symmetric];simp) apply (fastforce dest: silc_inv_initial_aag_reachable[OF reachable_Step'] simp: silc_inv_cur) apply (rule pas_wellformed_cur) apply (simp add: current_aag_def) apply (fastforce dest!: reachable_invs_if domains_distinct[THEN pas_domains_distinct_inj]
                       simp: invs_if_def Invs_def guarded_pas_domain_def
                             guarded_is_subject_cur_thread_def current_aag_def) apply (frule Step_current_aag_unchanged[symmetric];simp) apply (fastforce dest!: reachable_invs_if[OF reachable_Step']
                            domains_distinct[THEN pas_domains_distinct_inj]
                      simp: invs_if_def Invs_def guarded_pas_domain_def
                            guarded_is_subject_cur_thread_def current_aag_def) apply (rule partsSubjectAffects_bounds_those_subject_not_allowed_to_affect) apply (simp add: part_def partition_def current_aag_def split: if_split_asm) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s u s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s u s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (part s, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, s') \<in> same_for (current_aag (internal_state_if s)) u proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>reachable (a, b); ((a, b), aa, ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part (a, b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part (a, b) \<noteq> PSched; s = (a, b); s' = (aa, ba)\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> same_for (current_aag (snd a)) u proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> (((ab, bb), b), (ac, bc), ba) \<in> same_for (current_aag bb) u proof (prove)
goal (16 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_domains_distinct (current_aag bb)
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag bb) bb bc
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_refined (current_aag bb) bb
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_refined (current_aag bb) bc
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_objs bb
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_arch_state bc
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bb
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bc
 9. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 10. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag bb) bb bc
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_refined (current_aag bb) bb
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_refined (current_aag bb) bc
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_objs bb
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_arch_state bc
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bb
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bc
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 9. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 10. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_refined (current_aag bb) bb
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_refined (current_aag bb) bc
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_objs bb
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_arch_state bc
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bb
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bc
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 9. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 10. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_refined (current_aag bb) bc
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_objs bb
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_arch_state bc
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bb
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bc
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 9. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 10. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_objs bb
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_arch_state bc
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bb
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bc
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 9. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 10. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> valid_arch_state bc
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bb
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bc
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 9. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 10. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bb
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bc
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 9. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 10. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (9 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> einvs bc
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 9. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (8 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st4 a b aa ba ab bb ac bc) bb
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 8. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 a b aa ba ab bb ac bc) bc
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc); current_aag bb = current_aag (internal_state_if ((ac, bc), ba))\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) (?st'4 (ab, bb) b (ac, bc) ba ab bb ac bc) bc
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_wellformed_noninterference (current_aag bb)
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag bb) bb
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bb
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc); current_aag bb = current_aag (internal_state_if ((ac, bc), ba))\<rbrakk> \<Longrightarrow> guarded_is_subject_cur_thread (current_aag bb) bc
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<notin> partsSubjectAffects (pasPolicy (current_aag bb)) (label_of (pasSubject (current_aag bb)))
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> (Partition (label_of (pasSubject (current_aag bb))), u) \<notin> policyFlows (pasPolicy (current_aag bb))
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>reachable ((ab, bb), b); (((ab, bb), b), (ac, bc), ba) \<in> data_type.Step (big_step_ADT_A_if utf) (); (part ((ab, bb), b), u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched; part ((ab, bb), b) \<noteq> PSched; s = ((ab, bb), b); s' = ((ac, bc), ba); a = (ab, bb); aa = (ac, bc)\<rbrakk> \<Longrightarrow> u \<noteq> PSched proof (prove)
goal:
No subgoals!