theory Noninterference

lemma kernel_call_A_if_confidentiality:
  notes active_from_running[simp]
  shows "\<lbrakk> (s, t) \<in> uwr PSched; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u; invs_if s; invs_if t;
           invs_if s'; invs_if t'; (part s, u) \<in> policyFlows (pasPolicy initial_aag);
           part s \<noteq> PSched; u \<noteq> PSched; ((fst s),x,(fst s')) \<in> kernel_call_A_if e;
           ((fst t),y,(fst t')) \<in> kernel_call_A_if e; e \<noteq> Interrupt;
           sys_mode_of s = KernelEntry e; sys_mode_of t = KernelEntry e; snd s' = f x; snd t' = f y \<rbrakk>
           \<Longrightarrow> x = y \<and> (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s)" supply [[simp_depth_limit=3]] \<comment> \<open>speedup\<close> apply (frule (1) uwr_part_sys_mode_of_user_context_of_eq) apply (frule part_not_PSched_sys_mode_of_not_KernelSchedule_True) apply (clarsimp simp: kernel_call_A_if_def) apply (case_tac s, case_tac t, simp_all) apply (case_tac u, simp_all) apply (frule (6) uwr_reads_equiv_f_g_affects_equiv) apply (frule_tac s=b and t=ba and s2=b
                in use_ev[OF kernel_entry_if_reads_respects_f_g
                               [where st=s0_internal, OF current_domains_distinct]]) apply assumption apply (clarsimp simp: invs_if_def Invs_def schact_is_rct_def current_aag_def) apply assumption apply (clarsimp simp: invs_if_def Invs_def schact_is_rct_def
                           current_aag_eqI[OF uwr_PSched_cur_domain']) apply (simp add: current_aag_def) apply simp apply fastforce apply simp apply (rule reads_equiv_f_g_affects_equiv_uwr) apply simp+ apply (fastforce simp: invs_if_def Invs_def) apply simp apply simp apply (erule use_valid[OF _ kernel_entry_if_partitionIntegrity]) apply (clarsimp simp: partitionIntegrity_refl invs_if_def Invs_def current_aag_def
                           silc_inv_refl schact_is_rct_def guarded_pas_domain_def
                           ct_active_cur_thread_not_idle_thread[OF invs_valid_idle]) 
     (* XXX: the conjI is needed here -- metis won't instantiate a schematic var *)
      apply (rule conjI) apply (metis the_subject_of_aag_domain) apply assumption apply simp apply (erule use_valid[OF _ kernel_entry_if_partitionIntegrity]) apply (clarsimp simp: partitionIntegrity_refl invs_if_def Invs_def current_aag_def
                          silc_inv_refl schact_is_rct_def guarded_pas_domain_def
                          ct_active_cur_thread_not_idle_thread[OF invs_valid_idle]) 
    (* XXX: and here *)
     apply (rule conjI) apply (metis the_subject_of_aag_domain) apply assumption apply (simp add: sys_mode_of_def) apply (simp add: user_context_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; (fst s, x, fst s') \<in> kernel_call_A_if e; (fst t, y, fst t') \<in> kernel_call_A_if e; e \<noteq> Interrupt; sys_mode_of s = KernelEntry e; sys_mode_of t = KernelEntry e; snd s' = f x; snd t' = f y\<rbrakk> \<Longrightarrow> x = y \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; (fst s, x, fst s') \<in> kernel_call_A_if e; (fst t, y, fst t') \<in> kernel_call_A_if e; e \<noteq> Interrupt; sys_mode_of s = KernelEntry e; sys_mode_of t = KernelEntry e; snd s' = f x; snd t' = f y\<rbrakk> \<Longrightarrow> x = y \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; (fst s, x, fst s') \<in> kernel_call_A_if e; (fst t, y, fst t') \<in> kernel_call_A_if e; e \<noteq> Interrupt; sys_mode_of s = KernelEntry e; sys_mode_of t = KernelEntry e; snd s' = f x; snd t' = f y; sys_mode_of s = sys_mode_of t \<and> (user_modes (sys_mode_of s) \<longrightarrow> user_context_of s = user_context_of t)\<rbrakk> \<Longrightarrow> x = y \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; (fst s, x, fst s') \<in> kernel_call_A_if e; (fst t, y, fst t') \<in> kernel_call_A_if e; e \<noteq> Interrupt; sys_mode_of s = KernelEntry e; sys_mode_of t = KernelEntry e; snd s' = f x; snd t' = f y; sys_mode_of s = sys_mode_of t \<and> (user_modes (sys_mode_of s) \<longrightarrow> user_context_of s = user_context_of t); sys_mode_of s \<noteq> KernelSchedule True\<rbrakk> \<Longrightarrow> x = y \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba tc s'a tca s'aa r ra. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; e \<noteq> Interrupt; sys_mode_of t = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); sys_mode_of s = KernelEntry e; user_context_of s = user_context_of t; fst s = (a, b); fst t = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e a b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ())\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) u ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) u; part ((aa, b), KernelEntry e) \<noteq> PSched; u \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e)\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (6 subgoals):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> (?rv'37 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1, ?t'37 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) \<in> fst (kernel_entry_if e aa ba)
 2. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> (ct_active and silc_inv (current_aag b) s0_internal and einvs and only_timer_irq_inv (?irq38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) (?st'38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) and schact_is_rct and pas_refined (current_aag b) and pas_cur_domain (current_aag b) and guarded_pas_domain (current_aag b) and K (e \<noteq> Interrupt \<and> \<not> pasMaySendIrqs (current_aag b))) b
 3. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> (ct_active and silc_inv (current_aag b) s0_internal and einvs and only_timer_irq_inv (?irq38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) (?st'38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) and schact_is_rct and pas_refined (current_aag b) and pas_cur_domain (current_aag b) and guarded_pas_domain (current_aag b) and K (e \<noteq> Interrupt \<and> \<not> pasMaySendIrqs (current_aag b))) ba
 4. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag b) b ba
 5. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) b ba
 6. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)); ?rv'37 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1 = (r, tc) \<and> reads_equiv_f_g (current_aag b) s'a (?t'37 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) \<and> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) s'a (?t'37 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1)\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (5 subgoals):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> (ct_active and silc_inv (current_aag b) s0_internal and einvs and only_timer_irq_inv (?irq38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) (?st'38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) and schact_is_rct and pas_refined (current_aag b) and pas_cur_domain (current_aag b) and guarded_pas_domain (current_aag b) and K (e \<noteq> Interrupt \<and> \<not> pasMaySendIrqs (current_aag b))) b
 2. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> (ct_active and silc_inv (current_aag b) s0_internal and einvs and only_timer_irq_inv (?irq38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) (?st'38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) and schact_is_rct and pas_refined (current_aag b) and pas_cur_domain (current_aag b) and guarded_pas_domain (current_aag b) and K (e \<noteq> Interrupt \<and> \<not> pasMaySendIrqs (current_aag b))) ba
 3. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag b) b ba
 4. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) b ba
 5. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)); (ra, tca) = (r, tc) \<and> reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) s'a s'aa\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (5 subgoals):
 1. \<And>aa b ba tc s'a tca s'aa r ra x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; guarded_pas_domain initial_aag b; guarded_pas_domain initial_aag ba; guarded_pas_domain initial_aag s'a; guarded_pas_domain initial_aag s'aa; idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (ra = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (ra = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (ra = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> only_timer_irq_inv (?irq38 aa aa b ba tc s'a tca s'aa r ra (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) (?st'38 aa aa b ba tc s'a tca s'aa r ra (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) b
 2. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> (ct_active and silc_inv (current_aag b) s0_internal and einvs and only_timer_irq_inv (?irq38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) (?st'38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) and schact_is_rct and pas_refined (current_aag b) and pas_cur_domain (current_aag b) and guarded_pas_domain (current_aag b) and K (e \<noteq> Interrupt \<and> \<not> pasMaySendIrqs (current_aag b))) ba
 3. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag b) b ba
 4. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) b ba
 5. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)); (ra, tca) = (r, tc) \<and> reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) s'a s'aa\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> (ct_active and silc_inv (current_aag b) s0_internal and einvs and only_timer_irq_inv timer_irq s0_internal and schact_is_rct and pas_refined (current_aag b) and pas_cur_domain (current_aag b) and guarded_pas_domain (current_aag b) and K (e \<noteq> Interrupt \<and> \<not> pasMaySendIrqs (current_aag b))) ba
 2. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag b) b ba
 3. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) b ba
 4. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)); (ra, tca) = (r, tc) \<and> reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) s'a s'aa\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (4 subgoals):
 1. \<And>aa b ba tc s'a tca s'aa r ra x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (current_aag ba) b ba; affects_equiv (current_aag ba) (OrdinaryLabel x1) b ba; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (current_aag ba) s0_internal b; silc_inv (current_aag ba) s0_internal ba; silc_inv (current_aag s'a) s0_internal s'a; silc_inv (current_aag s'aa) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (current_aag ba) b; pas_refined (current_aag ba) ba; pas_refined (current_aag s'a) s'a; pas_refined (current_aag s'aa) s'aa; guarded_pas_domain (current_aag ba) b; guarded_pas_domain (current_aag ba) ba; guarded_pas_domain (current_aag s'a) s'a; guarded_pas_domain (current_aag s'aa) s'aa; idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (ra = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (ra = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (ra = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag ba) ba
 2. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag b) b ba
 3. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) b ba
 4. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)); (ra, tca) = (r, tc) \<and> reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) s'a s'aa\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag b) b ba
 2. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) b ba
 3. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)); (ra, tca) = (r, tc) \<and> reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) s'a s'aa\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) b ba
 2. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)); (ra, tca) = (r, tc) \<and> reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (?l38 a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1) s'a s'aa\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba tc s'a tca s'aa r ra ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (ra = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tca, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((ra, tca), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (ra = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)) \<and> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if ((aa, ba), KernelEntry e)); (ra, tca) = (r, tc) \<and> reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> (r = Inl ()) = (ra = Inl ()) \<and> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((aa, b), KernelEntry e)) t' proof (prove)
goal (10 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if s') (internal_state_if t')
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> affects_equiv (current_aag (internal_state_if ((aa, b), KernelEntry e))) (OrdinaryLabel x1) (internal_state_if s') (internal_state_if t')
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> policy2 (part ((aa, b), KernelEntry e)) (Partition x1)
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> part ((aa, b), KernelEntry e) \<noteq> PSched
 5. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s')
 6. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> uwr2 ((aa, b), KernelEntry e) PSched (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1)
 7. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if s')
 8. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1))) (internal_state_if (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1)) (internal_state_if t')
 9. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 10. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (6 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> silc_inv (current_aag s'a) s0_internal s'a
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> uwr2 ((aa, b), KernelEntry e) PSched (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1)
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if s')
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1))) (internal_state_if (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1)) (internal_state_if t')
 5. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 6. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (5 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> uwr2 ((aa, b), KernelEntry e) PSched (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1)
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if s')
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1))) (internal_state_if (?t220 a aa b ba tc s'a s'aa r ab bb ac bc x1)) (internal_state_if t')
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 5. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((aa, b), KernelEntry e))) (internal_state_if ((aa, b), KernelEntry e)) (internal_state_if s')
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (ac, bc))) (internal_state_if (ac, bc)) (internal_state_if t')
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b s'a
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (ac, bc))) (internal_state_if (ac, bc)) (internal_state_if t')
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> (silc_inv (current_aag b) b and pas_refined (current_aag b) and einvs and schact_is_rct and is_subject (current_aag b) \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs (current_aag b)) (?st'255 a aa b ba tc s'a s'aa r ab bb ac bc x1) and guarded_pas_domain (current_aag b) and (\<lambda>s. e \<noteq> Interrupt \<and> ct_active s) and (=) b) b
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (ac, bc))) (internal_state_if (ac, bc)) (internal_state_if t')
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread b) = the_elem (pasDomainAbs initial_aag (cur_domain b)) \<and> domain_sep_inv False (?st'255 aa aa b ba tc s'a s'aa r (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) b
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (ac, bc))) (internal_state_if (ac, bc)) (internal_state_if t')
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread b) = the_elem (pasDomainAbs initial_aag (cur_domain b)) \<and> domain_sep_inv False (?st'255 aa aa b ba tc s'a s'aa r (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) b
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (ac, bc))) (internal_state_if (ac, bc)) (internal_state_if t')
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (5 subgoals):
 1. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread b) = the_elem (pasDomainAbs initial_aag (cur_domain b))
 2. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st'255 aa aa b ba tc s'a s'aa r (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) b
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (ac, bc))) (internal_state_if (ac, bc)) (internal_state_if t')
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 5. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st'255 aa aa b ba tc s'a s'aa r (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) b
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (ac, bc))) (internal_state_if (ac, bc)) (internal_state_if t')
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (ac, bc))) (internal_state_if (ac, bc)) (internal_state_if t')
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag ba) ba s'aa
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> (silc_inv (current_aag ba) ba and pas_refined (current_aag ba) and einvs and schact_is_rct and is_subject (current_aag ba) \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs (current_aag ba)) (?st'347 a aa b ba tc s'a s'aa r ab bb ac bc x1) and guarded_pas_domain (current_aag ba) and (\<lambda>s. e \<noteq> Interrupt \<and> ct_active s) and (=) ba) ba
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread ba) = the_elem (pasDomainAbs initial_aag (cur_domain ba)) \<and> domain_sep_inv False (?st'347 aa aa b ba tc s'a s'aa r (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) ba
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread ba) = the_elem (pasDomainAbs initial_aag (cur_domain ba)) \<and> domain_sep_inv False (?st'347 aa aa b ba tc s'a s'aa r (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) ba
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread ba) = the_elem (pasDomainAbs initial_aag (cur_domain ba))
 2. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st'347 aa aa b ba tc s'a s'aa r (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) ba
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>aa b ba tc s'a s'aa r x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; invs b; invs ba; invs s'a; invs s'aa; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b ba; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) b ba; reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s'a s'aa; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) (OrdinaryLabel x1) s'a s'aa; valid_list b; valid_list ba; valid_list s'a; valid_list s'aa; valid_sched_2 (ready_queues b) (ekheap b) resume_cur_thread (cur_domain b) (kheap b) (cur_thread b) (idle_thread b); valid_sched_2 (ready_queues ba) (ekheap ba) resume_cur_thread (cur_domain ba) (kheap ba) (cur_thread ba) (idle_thread ba); valid_sched s'a; valid_sched s'aa; only_timer_irq_inv timer_irq s0_internal b; only_timer_irq_inv timer_irq s0_internal ba; only_timer_irq_inv timer_irq s0_internal s'a; only_timer_irq_inv timer_irq s0_internal s'aa; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) s0_internal b; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) s0_internal ba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s0_internal s'a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s0_internal s'aa; domain_sep_inv False s0_internal b; domain_sep_inv False s0_internal ba; domain_sep_inv False s0_internal s'a; domain_sep_inv False s0_internal s'aa; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain b))\<rparr>) b; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ba))\<rparr>) ba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'a))\<rparr>) s'a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s'aa))\<rparr>) s'aa; pasObjectAbs initial_aag (cur_thread b) \<in> pasDomainAbs initial_aag (cur_domain b); pasObjectAbs initial_aag (cur_thread ba) \<in> pasDomainAbs initial_aag (cur_domain ba); cur_thread s'a \<noteq> idle_thread s'a \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'a) \<in> pasDomainAbs initial_aag (cur_domain s'a); cur_thread s'aa \<noteq> idle_thread s'aa \<longrightarrow> pasObjectAbs initial_aag (cur_thread s'aa) \<in> pasDomainAbs initial_aag (cur_domain s'aa); idle_equiv s0_internal b; idle_equiv s0_internal ba; idle_equiv s0_internal s'a; idle_equiv s0_internal s'aa; valid_domain_list b; valid_domain_list ba; valid_domain_list s'a; valid_domain_list s'aa; valid_vspace_objs_if b; valid_vspace_objs_if ba; valid_vspace_objs_if s'a; valid_vspace_objs_if s'aa; det_inv (KernelEntry e) (cur_thread_context_of ((aa, b), KernelEntry e)) b; det_inv (KernelEntry e) (cur_thread_context_of ((aa, ba), KernelEntry e)) ba; det_inv (sys_mode_of s') (cur_thread_context_of s') s'a; det_inv (sys_mode_of t') (cur_thread_context_of t') s'aa; 0 < domain_time b; 0 < domain_time ba; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'a; f (r = Inl ()) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time s'aa; domain_time b \<noteq> 0; domain_time ba \<noteq> 0; domain_time s'a = 0 \<longrightarrow> scheduler_action s'a = choose_new_thread; domain_time s'aa = 0 \<longrightarrow> scheduler_action s'aa = choose_new_thread; ct_idle b \<longrightarrow> aa = idle_context b; ct_idle ba \<longrightarrow> aa = idle_context ba; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'a \<longrightarrow> user_context_of s' = idle_context s'a; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True; f (r = Inl ()) \<noteq> KernelExit \<longrightarrow> ct_idle s'aa \<longrightarrow> user_context_of t' = idle_context s'aa; case f (r = Inl ()) of InUserMode \<Rightarrow> ct_running (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t') \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t')) \<and> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t') \<or> ct_idle (internal_state_if t')) \<and> scheduler_action (internal_state_if t') = resume_cur_thread | _ \<Rightarrow> True; ct_running b; ct_running ba; scheduler_action b = resume_cur_thread; scheduler_action ba = resume_cur_thread\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st'347 aa aa b ba tc s'a s'aa r (aa, b) (KernelEntry e) (aa, ba) (KernelEntry e) x1) ba
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 2. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba tc s'a s'aa r ab bb ac bc x1. \<lbrakk>uwr2 ((aa, b), KernelEntry e) PSched ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (part ((aa, b), KernelEntry e)) ((aa, ba), KernelEntry e); uwr2 ((aa, b), KernelEntry e) (Partition x1) ((aa, ba), KernelEntry e); invs_if ((aa, b), KernelEntry e); invs_if ((aa, ba), KernelEntry e); invs_if s'; invs_if t'; policy2 (part ((aa, b), KernelEntry e)) (Partition x1); part ((aa, b), KernelEntry e) \<noteq> PSched; e \<noteq> Interrupt; bc = KernelEntry e; snd s' = f (r = Inl ()); snd t' = f (r = Inl ()); bb = KernelEntry e; a = aa; ab = (aa, b); ac = (aa, ba); fst s' = (tc, s'a); fst t' = (tc, s'aa); ((r, tc), s'a) \<in> fst (kernel_entry_if e aa b); x = (r = Inl ()); ((r, tc), s'aa) \<in> fst (kernel_entry_if e aa ba); y = (r = Inl ()); s = ((aa, b), KernelEntry e); t = ((aa, ba), KernelEntry e); u = Partition x1; reads_equiv_f_g (current_aag b) b ba \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) b ba; reads_equiv_f_g (current_aag b) s'a s'aa \<and> affects_equiv (current_aag b) (OrdinaryLabel x1) s'a s'aa\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal:
No subgoals!