theory Noninterference

lemma confidentiality_for_sched:
  "\<lbrakk> (s, t) \<in> uwr PSched;
     system.reachable (big_step_ADT_A_if utf) s0 s; system.reachable (big_step_ADT_A_if utf) s0 t;
     (s, s') \<in> Simulation.Step (big_step_ADT_A_if utf) ();
     (t, t') \<in> Simulation.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> (s', t') \<in> uwr PSched" apply (frule schedIncludesCurrentDom) apply (frule_tac s=s in reachable_nonsched_exit,assumption) apply (frule_tac s=t in reachable_nonsched_exit,simp) apply (frule_tac s=s and s'=s' in Step_partitionIntegrity,simp+) apply (frule_tac s=t and s'=t' in Step_partitionIntegrity,simp+) apply (simp add: uwr_def sameFor_def) apply (simp add: sameFor_scheduler_def) apply clarsimp apply (case_tac s') apply clarsimp apply (case_tac t') apply clarsimp apply (clarsimp simp add: partitionIntegrity_def) apply (rule conjI) apply (metis domain_fields_equiv_sym domain_fields_equiv_trans) apply (rule conjI) apply (metis globals_equiv_scheduler_sym globals_equiv_scheduler_trans) apply (rule conjI) apply (fold silc_dom_equiv_def) apply (simp add: silc_dom_equiv_current_aag) apply (metis silc_dom_equiv_sym silc_dom_equiv_trans) apply (rule conjI) apply (rule trans) apply (rule sym) apply (rule_tac ?s1.0="((a, b), KernelExit)" in big_step_irq_state_next_irq) apply (simp add: reachable_invs_if) apply (simp add: big_step_R_rtranclp) apply simp+ apply (subgoal_tac "irq_masks_of_state b = irq_masks_of_state bb") apply simp apply (rule_tac ?s1.0="((aa, bb), KernelExit)" in big_step_irq_state_next_irq) apply (simp add: reachable_invs_if) apply (simp add: big_step_R_rtranclp) apply simp+ apply (rule trans) apply (rule irq_masks_constant,assumption,fastforce) apply (rule sym) apply (rule irq_masks_constant,assumption,fastforce) apply (simp add: Step_big_step_ADT_A_if) apply (erule big_stepsE) apply (erule big_stepsE) apply (simp add: big_step_R_def) apply (case_tac baa, simp_all) apply (case_tac bca, simp_all) apply (case_tac bca, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched; part s = part t\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched; part s = part t; snd s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched; part s = part t; snd s = KernelExit; snd t = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part t \<noteq> PSched; part s = part t; snd s = KernelExit; snd t = KernelExit; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s')\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part t \<noteq> PSched; part s = part t; snd s = KernelExit; snd t = KernelExit; 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')\<rbrakk> \<Longrightarrow> uwr2 s' PSched t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> sameFor_scheduler (pasPolicy initial_aag) (pasObjectAbs initial_aag) (pasIRQAbs initial_aag) (pasASIDAbs initial_aag) (pasDomainAbs initial_aag); reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part t \<noteq> PSched; part s = part t; snd s = KernelExit; snd t = KernelExit; 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')\<rbrakk> \<Longrightarrow> (s', t') \<in> sameFor_scheduler (pasPolicy initial_aag) (pasObjectAbs initial_aag) (pasIRQAbs initial_aag) (pasASIDAbs initial_aag) (pasDomainAbs initial_aag) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>a b ba. s = ((a, b), ba) \<and> (\<exists>a bb bc. t = ((a, bb), bc) \<and> domain_fields_equiv b bb \<and> idle_thread b = idle_thread bb \<and> globals_equiv_scheduler b bb \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> scheduler_modes ba = scheduler_modes bc \<and> interrupted_modes ba = interrupted_modes bc); reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part t \<noteq> PSched; part s = part t; snd s = KernelExit; snd t = KernelExit; 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')\<rbrakk> \<Longrightarrow> \<exists>a b ba. s' = ((a, b), ba) \<and> (\<exists>a bb bc. t' = ((a, bb), bc) \<and> domain_fields_equiv b bb \<and> idle_thread b = idle_thread bb \<and> globals_equiv_scheduler b bb \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> scheduler_modes ba = scheduler_modes bc \<and> interrupted_modes ba = interrupted_modes bc) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); partitionIntegrity (current_aag b) b (internal_state_if s'); partitionIntegrity (current_aag bb) bb (internal_state_if t'); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bb; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb)\<rbrakk> \<Longrightarrow> \<exists>a b ba. s' = ((a, b), ba) \<and> (\<exists>a bb bc. t' = ((a, bb), bc) \<and> domain_fields_equiv b bb \<and> idle_thread b = idle_thread bb \<and> globals_equiv_scheduler b bb \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> scheduler_modes ba = scheduler_modes bc \<and> interrupted_modes ba = interrupted_modes bc) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); partitionIntegrity (current_aag b) b (internal_state_if s'); partitionIntegrity (current_aag bb) bb (internal_state_if t'); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bb; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = (ab, ba)\<rbrakk> \<Longrightarrow> \<exists>a b ba. s' = ((a, b), ba) \<and> (\<exists>a bb bc. t' = ((a, bb), bc) \<and> domain_fields_equiv b bb \<and> idle_thread b = idle_thread bb \<and> globals_equiv_scheduler b bb \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> scheduler_modes ba = scheduler_modes bc \<and> interrupted_modes ba = interrupted_modes bc) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); partitionIntegrity (current_aag b) b ba; partitionIntegrity (current_aag bb) bb (internal_state_if t'); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bb; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa)\<rbrakk> \<Longrightarrow> \<exists>a b bb. t' = ((a, b), bb) \<and> domain_fields_equiv ba b \<and> idle_thread ba = idle_thread b \<and> globals_equiv_scheduler ba b \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba b \<and> equiv_irq_state (machine_state ba) (machine_state b) \<and> scheduler_modes baa = scheduler_modes bb \<and> interrupted_modes baa = interrupted_modes bb proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), t') \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); partitionIntegrity (current_aag b) b ba; partitionIntegrity (current_aag bb) bb (internal_state_if t'); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bb; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = (ac, bc)\<rbrakk> \<Longrightarrow> \<exists>a b bb. t' = ((a, b), bb) \<and> domain_fields_equiv ba b \<and> idle_thread ba = idle_thread b \<and> globals_equiv_scheduler ba b \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba b \<and> equiv_irq_state (machine_state ba) (machine_state b) \<and> scheduler_modes baa = scheduler_modes bb \<and> interrupted_modes baa = interrupted_modes bb proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); partitionIntegrity (current_aag b) b ba; partitionIntegrity (current_aag bb) bb bc; s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bb; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca)\<rbrakk> \<Longrightarrow> domain_fields_equiv ba bc \<and> idle_thread ba = idle_thread bc \<and> globals_equiv_scheduler ba bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba bc \<and> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> domain_fields_equiv ba bc \<and> globals_equiv_scheduler ba bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba bc \<and> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> domain_fields_equiv ba bc
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> globals_equiv_scheduler ba bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba bc \<and> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> globals_equiv_scheduler ba bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba bc \<and> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> globals_equiv_scheduler ba bc
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba bc \<and> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba bc \<and> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap ba bc
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> silc_dom_equiv initial_aag ba bc
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv initial_aag b ba; globals_equiv_scheduler bb bc; silc_dom_equiv initial_aag bb bc\<rbrakk> \<Longrightarrow> silc_dom_equiv initial_aag ba bc
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> equiv_irq_state (machine_state ba) (machine_state bc) \<and> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> equiv_irq_state (machine_state ba) (machine_state bc)
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (3 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_state_of_state ba = ?s61 a b aa bb ab ba baa ac bc bca
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ?s61 a b aa bb ab ba baa ac bc bca = irq_state_of_state bc
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (3 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ?s61 a b aa bb ab ba baa ac bc bca = irq_state_of_state ba
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ?s61 a b aa bb ab ba baa ac bc bca = irq_state_of_state bc
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (8 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> invs_if ((a, b), KernelExit)
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 ((a, b), KernelExit)
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> (((a, b), KernelExit), ?s2.66 a b aa bb ab ba baa ac bc bca) \<in> data_type.Step (big_step_ADT_A_if utf) (?a66 a b aa bb ab ba baa ac bc bca)
 4. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> snd ((a, b), KernelExit) = KernelExit
 5. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ?i_s1.66 a b aa bb ab ba baa ac bc bca = internal_state_if ((a, b), KernelExit)
 6. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ba = internal_state_if (?s2.66 a b aa bb ab ba baa ac bc bca)
 7. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> next_irq_state_of_state (?i_s1.66 a b aa bb ab ba baa ac bc bca) = irq_state_of_state bc
 8. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (7 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 ((a, b), KernelExit)
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> (((a, b), KernelExit), ?s2.66 a b aa bb ab ba baa ac bc bca) \<in> data_type.Step (big_step_ADT_A_if utf) (?a66 a b aa bb ab ba baa ac bc bca)
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> snd ((a, b), KernelExit) = KernelExit
 4. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ?i_s1.66 a b aa bb ab ba baa ac bc bca = internal_state_if ((a, b), KernelExit)
 5. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ba = internal_state_if (?s2.66 a b aa bb ab ba baa ac bc bca)
 6. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> next_irq_state_of_state (?i_s1.66 a b aa bb ab ba baa ac bc bca) = irq_state_of_state bc
 7. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (6 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> (((a, b), KernelExit), ?s2.66 a b aa bb ab ba baa ac bc bca) \<in> data_type.Step (big_step_ADT_A_if utf) (?a66 a b aa bb ab ba baa ac bc bca)
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> snd ((a, b), KernelExit) = KernelExit
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ?i_s1.66 a b aa bb ab ba baa ac bc bca = internal_state_if ((a, b), KernelExit)
 4. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ba = internal_state_if (?s2.66 a b aa bb ab ba baa ac bc bca)
 5. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> next_irq_state_of_state (?i_s1.66 a b aa bb ab ba baa ac bc bca) = irq_state_of_state bc
 6. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> next_irq_state (Suc (irq_state_of_state bb)) (irq_masks_of_state b) = irq_state_of_state bc
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (3 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> next_irq_state (Suc (irq_state_of_state bb)) (irq_masks_of_state b) = irq_state_of_state bc
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state bb
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (3 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> next_irq_state_of_state bb = irq_state_of_state bc
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state bb
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (8 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> invs_if ((aa, bb), KernelExit)
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 ((aa, bb), KernelExit)
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> (((aa, bb), KernelExit), ?s2.69 a b aa bb ab ba baa ac bc bca) \<in> data_type.Step (big_step_ADT_A_if utf) (?a69 a b aa bb ab ba baa ac bc bca)
 4. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> snd ((aa, bb), KernelExit) = KernelExit
 5. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> bb = internal_state_if ((aa, bb), KernelExit)
 6. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> bc = internal_state_if (?s2.69 a b aa bb ab ba baa ac bc bca)
 7. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state bb
 8. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (7 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 ((aa, bb), KernelExit)
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> (((aa, bb), KernelExit), ?s2.69 a b aa bb ab ba baa ac bc bca) \<in> data_type.Step (big_step_ADT_A_if utf) (?a69 a b aa bb ab ba baa ac bc bca)
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> snd ((aa, bb), KernelExit) = KernelExit
 4. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> bb = internal_state_if ((aa, bb), KernelExit)
 5. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> bc = internal_state_if (?s2.69 a b aa bb ab ba baa ac bc bca)
 6. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state bb
 7. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (6 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> (((aa, bb), KernelExit), ?s2.69 a b aa bb ab ba baa ac bc bca) \<in> data_type.Step (big_step_ADT_A_if utf) (?a69 a b aa bb ab ba baa ac bc bca)
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> snd ((aa, bb), KernelExit) = KernelExit
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> bb = internal_state_if ((aa, bb), KernelExit)
 4. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; irq_masks_of_state b = irq_masks_of_state bb\<rbrakk> \<Longrightarrow> bc = internal_state_if (?s2.69 a b aa bb ab ba baa ac bc bca)
 5. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state bb
 6. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state bb
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (3 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state b = ?s70 a b aa bb ab ba baa ac bc bca
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> ?s70 a b aa bb ab ba baa ac bc bca = irq_masks_of_state bb
 3. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s0) = irq_masks_of_state bb
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> irq_masks_of_state bb = irq_masks_of_state (internal_state_if s0)
 2. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> data_type.Step (big_step_ADT_A_if utf) (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> data_type.Step (big_step_ADT_A_if utf) (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((a, b), KernelExit), (ab, ba), baa) \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap (); (((aa, bb), KernelExit), (ac, bc), bca) \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca s'a as ad. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); (((aa, bb), KernelExit), (ac, bc), bca) \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap (); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), KernelExit); (s'a, (ab, ba), baa) \<in> data_type.Step (ADT_A_if utf) ad; big_step_R ((a, b), KernelExit) ((ab, ba), baa); () = big_step_evmap (as @ [ad])\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca s'a as ad s'aa asa ae. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), KernelExit); (s'a, (ab, ba), baa) \<in> data_type.Step (ADT_A_if utf) ad; big_step_R ((a, b), KernelExit) ((ab, ba), baa); () = big_step_evmap (as @ [ad]); (s'aa, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((aa, bb), KernelExit); (s'aa, (ac, bc), bca) \<in> data_type.Step (ADT_A_if utf) ae; big_step_R ((aa, bb), KernelExit) ((ac, bc), bca); () = big_step_evmap (asa @ [ae])\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca \<and> interrupted_modes baa = interrupted_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca s'a as s'aa asa. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), baa); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) ((a, b), KernelExit); (s'a, (ab, ba), baa) \<in> data_type.Step (ADT_A_if utf) (); interrupted_modes baa; (s'aa, asa) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) ((aa, bb), KernelExit); (s'aa, (ac, bc), bca) \<in> data_type.Step (ADT_A_if utf) (); interrupted_modes bca\<rbrakk> \<Longrightarrow> scheduler_modes baa = scheduler_modes bca proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ba baa ac bc bca s'a as s'aa asa x3. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), KernelEntry Interrupt); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) ((a, b), KernelExit); (s'a, (ab, ba), KernelEntry Interrupt) \<in> data_type.Step (ADT_A_if utf) (); x3 = Interrupt; (s'aa, asa) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) ((aa, bb), KernelExit); (s'aa, (ac, bc), bca) \<in> data_type.Step (ADT_A_if utf) (); interrupted_modes bca; baa = KernelEntry Interrupt\<rbrakk> \<Longrightarrow> scheduler_modes bca
 2. \<And>a b aa bb ab ba baa ac bc bca s'a as s'aa asa. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), KernelPreempted); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) ((a, b), KernelExit); (s'a, (ab, ba), KernelPreempted) \<in> data_type.Step (ADT_A_if utf) (); (s'aa, asa) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) ((aa, bb), KernelExit); (s'aa, (ac, bc), bca) \<in> data_type.Step (ADT_A_if utf) (); interrupted_modes bca; baa = KernelPreempted\<rbrakk> \<Longrightarrow> scheduler_modes bca proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ba baa ac bc bca s'a as s'aa asa. \<lbrakk>reachable ((a, b), KernelExit); reachable ((aa, bb), KernelExit); part ((aa, bb), KernelExit) \<noteq> PSched; part ((a, b), KernelExit) = part ((aa, bb), KernelExit); s = ((a, b), KernelExit); t = ((aa, bb), KernelExit); domain_fields_equiv b bb; idle_thread b = idle_thread bc; globals_equiv_scheduler b bb; silc_dom_equiv initial_aag b bb; equiv_irq_state (machine_state b) (machine_state bb); s' = ((ab, ba), KernelPreempted); t' = ((ac, bc), bca); integrity_subjects {pasSubject (current_aag b)} (current_aag b\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} b ba; integrity_subjects {pasSubject (current_aag bb)} (current_aag bb\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} bb bc; domain_fields_equiv b ba; domain_fields_equiv bb bc; idle_thread bb = idle_thread bc; idle_thread ba = idle_thread bc; globals_equiv_scheduler b ba; silc_dom_equiv (current_aag b) b ba; globals_equiv_scheduler bb bc; silc_dom_equiv (current_aag bb) bb bc; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) ((a, b), KernelExit); (s'a, (ab, ba), KernelPreempted) \<in> data_type.Step (ADT_A_if utf) (); (s'aa, asa) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) ((aa, bb), KernelExit); (s'aa, (ac, bc), bca) \<in> data_type.Step (ADT_A_if utf) (); interrupted_modes bca; baa = KernelPreempted\<rbrakk> \<Longrightarrow> scheduler_modes bca proof (prove)
goal:
No subgoals!