theory Noninterference

lemma kernel_exit_A_if_confidentiality:
  "\<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_exit_A_if;
    ((fst t),y,(fst t')) \<in> kernel_exit_A_if;
    sys_mode_of s = KernelExit; sys_mode_of t = KernelExit;
    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=2]] \<comment> \<open>speedup\<close> apply (clarsimp simp: kernel_exit_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 (simp split: prod.splits) apply (case_tac "fst s'", simp) apply (case_tac "fst t'", simp) apply (frule_tac s=x2 and t=x2a and aag1="current_aag x2"
                in use_ev2[OF kernel_exit_if_reads_respects_f_g_2[where st=s0_internal]]) apply assumption apply (clarsimp simp: invs_if_def Invs_def current_aag_def guarded_pas_domain_def) apply (metis the_subject_of_aag_domain) apply (clarsimp simp: invs_if_def Invs_def) apply (drule uwr_PSched_cur_domain) apply (clarsimp simp: current_aag_def guarded_pas_domain_def) apply (metis the_subject_of_aag_domain) apply simp apply fastforce apply simp apply (elim conjE) apply (drule state_unchanged[OF kernel_exit_if_inv])+ apply (subgoal_tac "ct_running bb = ct_running bc") 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 (rule partitionIntegrity_refl) apply simp apply (rule partitionIntegrity_refl) apply (simp add: sys_mode_of_def) apply (simp add: user_context_of_def) apply (frule_tac bd=bb in reads_equiv_g_ct_running_eq[OF reads_equiv_f_g_reads_equiv_g]) apply (fastforce simp: invs_if_def) apply (fastforce simp: invs_if_def) apply (fastforce simp: reads_equiv_f_g_def reads_equiv_def current_aag_def) apply simp 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_exit_A_if; (fst t, y, fst t') \<in> kernel_exit_A_if; sys_mode_of s = KernelExit; sys_mode_of t = KernelExit; 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_exit_A_if; (fst t, y, fst t') \<in> kernel_exit_A_if; sys_mode_of s = KernelExit; sys_mode_of t = KernelExit; 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; sys_mode_of s = KernelExit; sys_mode_of t = KernelExit; snd s' = f (if ct_running (internal_state_if s') then InUserMode else InIdleMode); snd t' = f (if ct_running (internal_state_if t') then InUserMode else InIdleMode); fst s' \<in> fst (case fst s of (x, xa) \<Rightarrow> kernel_exit_if x xa); x = (if ct_running (internal_state_if s') then InUserMode else InIdleMode); fst t' \<in> fst (case fst t of (x, xa) \<Rightarrow> kernel_exit_if x xa); y = (if ct_running (internal_state_if t') then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> (ct_running (internal_state_if s') \<longrightarrow> (ct_running (internal_state_if t') \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t') \<and> ct_running (internal_state_if t')) \<and> (\<not> ct_running (internal_state_if s') \<longrightarrow> \<not> ct_running (internal_state_if t') \<and> (\<not> ct_running (internal_state_if t') \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>uwr2 (a, b) PSched (aa, ba); uwr2 (a, b) (part (a, b)) (aa, ba); uwr2 (a, b) u (aa, ba); invs_if (a, b); invs_if (aa, ba); invs_if s'; invs_if t'; policy2 (part (a, b)) u; part (a, b) \<noteq> PSched; u \<noteq> PSched; sys_mode_of (a, b) = KernelExit; sys_mode_of (aa, ba) = KernelExit; snd s' = f (if ct_running (internal_state_if s') then InUserMode else InIdleMode); snd t' = f (if ct_running (internal_state_if t') then InUserMode else InIdleMode); fst s' \<in> fst (case a of (x, xa) \<Rightarrow> kernel_exit_if x xa); x = (if ct_running (internal_state_if s') then InUserMode else InIdleMode); fst t' \<in> fst (case aa of (x, xa) \<Rightarrow> kernel_exit_if x xa); y = (if ct_running (internal_state_if t') then InUserMode else InIdleMode); s = (a, b); t = (aa, ba)\<rbrakk> \<Longrightarrow> (ct_running (internal_state_if s') \<longrightarrow> (ct_running (internal_state_if t') \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part (a, b)) t') \<and> ct_running (internal_state_if t')) \<and> (\<not> ct_running (internal_state_if s') \<longrightarrow> \<not> ct_running (internal_state_if t') \<and> (\<not> ct_running (internal_state_if t') \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part (a, b)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1. \<lbrakk>uwr2 (a, b) PSched (aa, ba); uwr2 (a, b) (part (a, b)) (aa, ba); uwr2 (a, b) (Partition x1) (aa, ba); invs_if (a, b); invs_if (aa, ba); invs_if s'; invs_if t'; policy2 (part (a, b)) (Partition x1); part (a, b) \<noteq> PSched; sys_mode_of (a, b) = KernelExit; sys_mode_of (aa, ba) = KernelExit; snd s' = f (if ct_running (internal_state_if s') then InUserMode else InIdleMode); snd t' = f (if ct_running (internal_state_if t') then InUserMode else InIdleMode); fst s' \<in> fst (case a of (x, xa) \<Rightarrow> kernel_exit_if x xa); x = (if ct_running (internal_state_if s') then InUserMode else InIdleMode); fst t' \<in> fst (case aa of (x, xa) \<Rightarrow> kernel_exit_if x xa); y = (if ct_running (internal_state_if t') then InUserMode else InIdleMode); s = (a, b); t = (aa, ba); u = Partition x1\<rbrakk> \<Longrightarrow> (ct_running (internal_state_if s') \<longrightarrow> (ct_running (internal_state_if t') \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part (a, b)) t') \<and> ct_running (internal_state_if t')) \<and> (\<not> ct_running (internal_state_if s') \<longrightarrow> \<not> ct_running (internal_state_if t') \<and> (\<not> ct_running (internal_state_if t') \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part (a, b)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1. \<lbrakk>uwr2 (a, b) PSched (aa, ba); uwr2 (a, b) (part (a, b)) (aa, ba); uwr2 (a, b) (Partition x1) (aa, ba); invs_if (a, b); invs_if (aa, ba); invs_if s'; invs_if t'; policy2 (part (a, b)) (Partition x1); part (a, b) \<noteq> PSched; sys_mode_of (a, b) = KernelExit; sys_mode_of (aa, ba) = KernelExit; snd s' = f (if ct_running (internal_state_if s') then InUserMode else InIdleMode); snd t' = f (if ct_running (internal_state_if t') then InUserMode else InIdleMode); fst s' \<in> fst (case a of (x, xa) \<Rightarrow> kernel_exit_if x xa); x = (if ct_running (internal_state_if s') then InUserMode else InIdleMode); fst t' \<in> fst (case aa of (x, xa) \<Rightarrow> kernel_exit_if x xa); y = (if ct_running (internal_state_if t') then InUserMode else InIdleMode); s = (a, b); t = (aa, ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if (a, b))) (internal_state_if (a, b)) (internal_state_if (aa, ba)) \<and> affects_equiv (current_aag (internal_state_if (a, b))) (OrdinaryLabel x1) (internal_state_if (a, b)) (internal_state_if (aa, ba))\<rbrakk> \<Longrightarrow> (ct_running (internal_state_if s') \<longrightarrow> (ct_running (internal_state_if t') \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part (a, b)) t') \<and> ct_running (internal_state_if t')) \<and> (\<not> ct_running (internal_state_if s') \<longrightarrow> \<not> ct_running (internal_state_if t') \<and> (\<not> ct_running (internal_state_if t') \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part (a, b)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a. \<lbrakk>y = (if ct_running (internal_state_if t') then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running (internal_state_if s') then InUserMode else InIdleMode); snd t' = f (if ct_running (internal_state_if t') then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); fst s' \<in> fst (kernel_exit_if x1a x2); x = (if ct_running (internal_state_if s') then InUserMode else InIdleMode); aa = (x1b, x2a); fst t' \<in> fst (kernel_exit_if x1b x2a)\<rbrakk> \<Longrightarrow> (ct_running (internal_state_if s') \<longrightarrow> (ct_running (internal_state_if t') \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running (internal_state_if t')) \<and> (\<not> ct_running (internal_state_if s') \<longrightarrow> \<not> ct_running (internal_state_if t') \<and> (\<not> ct_running (internal_state_if t') \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb. \<lbrakk>y = (if ct_running (internal_state_if t') then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running (internal_state_if t') then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst t' \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb)\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running (internal_state_if t') \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running (internal_state_if t')) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running (internal_state_if t') \<and> (\<not> ct_running (internal_state_if t') \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> (?rv'46 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc, ?t'46 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) \<in> fst (kernel_exit_if (?tc'47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2a)
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> (silc_inv (current_aag x2) s0_internal and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject (current_aag x2) (cur_thread s))) x2
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> (silc_inv (current_aag x2) s0_internal and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject (current_aag x2) (cur_thread s))) x2a
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag x2) x2 x2a
 5. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 6. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ?rv'46 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc \<and> reads_equiv_f_g (current_aag x2) bb (?t'46 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb (?t'46 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc)\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> (silc_inv (current_aag x2) s0_internal and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject (current_aag x2) (cur_thread s))) x2
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> (silc_inv (current_aag x2) s0_internal and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject (current_aag x2) (cur_thread s))) x2a
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag x2) x2 x2a
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 5. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (5 subgoals):
 1. \<And>x1 x1a x2 x1b x2a ab bba ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; snd s' = f (if ct_running bba then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2))\<rparr>) x2 x2a; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2))\<rparr>) (OrdinaryLabel x1) x2 x2a; (ab, bba) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bba then InUserMode else InIdleMode); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bba); fst t' = (ac, bc); invs x2; invs x2a; invs bba; invs bc; valid_list x2; valid_list x2a; valid_list bba; valid_list bc; valid_sched_2 (ready_queues x2) (ekheap x2) resume_cur_thread (cur_domain x2) (kheap x2) (cur_thread x2) (idle_thread x2); valid_sched_2 (ready_queues x2a) (ekheap x2a) resume_cur_thread (cur_domain x2a) (kheap x2a) (cur_thread x2a) (idle_thread x2a); valid_sched bba; valid_sched bc; only_timer_irq_inv timer_irq s0_internal x2; only_timer_irq_inv timer_irq s0_internal x2a; only_timer_irq_inv timer_irq s0_internal bba; only_timer_irq_inv timer_irq s0_internal bc; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2))\<rparr>) s0_internal x2; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rparr>) s0_internal x2a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bba))\<rparr>) s0_internal bba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bc))\<rparr>) s0_internal bc; domain_sep_inv False s0_internal x2; domain_sep_inv False s0_internal x2a; domain_sep_inv False s0_internal bba; domain_sep_inv False s0_internal bc; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2))\<rparr>) x2; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rparr>) x2a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bba))\<rparr>) bba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bc))\<rparr>) bc; cur_thread x2 \<noteq> idle_thread x2 \<longrightarrow> pasObjectAbs initial_aag (cur_thread x2) \<in> pasDomainAbs initial_aag (cur_domain x2); cur_thread x2a \<noteq> idle_thread x2a \<longrightarrow> pasObjectAbs initial_aag (cur_thread x2a) \<in> pasDomainAbs initial_aag (cur_domain x2a); cur_thread bba \<noteq> idle_thread bba \<longrightarrow> pasObjectAbs initial_aag (cur_thread bba) \<in> pasDomainAbs initial_aag (cur_domain bba); cur_thread bc \<noteq> idle_thread bc \<longrightarrow> pasObjectAbs initial_aag (cur_thread bc) \<in> pasDomainAbs initial_aag (cur_domain bc); idle_equiv s0_internal x2; idle_equiv s0_internal x2a; idle_equiv s0_internal bba; idle_equiv s0_internal bc; valid_domain_list x2; valid_domain_list x2a; valid_domain_list bba; valid_domain_list bc; valid_vspace_objs_if x2; valid_vspace_objs_if x2a; valid_vspace_objs_if bba; valid_vspace_objs_if bc; det_inv KernelExit (cur_thread_context_of ((x1a, x2), KernelExit)) x2; det_inv KernelExit (cur_thread_context_of ((x1b, x2a), KernelExit)) x2a; det_inv (sys_mode_of s') (cur_thread_context_of s') bba; det_inv (sys_mode_of t') (cur_thread_context_of t') bc; 0 < domain_time x2; 0 < domain_time x2a; f (if ct_running bba then InUserMode else InIdleMode) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time bba; f (if ct_running bc then InUserMode else InIdleMode) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time bc; domain_time x2 \<noteq> 0; domain_time x2a \<noteq> 0; domain_time bba = 0 \<longrightarrow> scheduler_action bba = choose_new_thread; domain_time bc = 0 \<longrightarrow> scheduler_action bc = choose_new_thread; ct_running x2 \<or> ct_idle x2; scheduler_action x2 = resume_cur_thread; ct_running x2a \<or> ct_idle x2a; scheduler_action x2a = resume_cur_thread; f (if ct_running bba then InUserMode else InIdleMode) \<noteq> KernelExit \<longrightarrow> ct_idle bba \<longrightarrow> user_context_of s' = idle_context bba; case f (if ct_running bba then InUserMode else InIdleMode) 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 (if ct_running bc then InUserMode else InIdleMode) \<noteq> KernelExit \<longrightarrow> ct_idle bc \<longrightarrow> user_context_of t' = idle_context bc; case f (if ct_running bc then InUserMode else InIdleMode) 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; pasObjectAbs initial_aag (cur_thread x2) \<noteq> the_elem (pasDomainAbs initial_aag (cur_domain x2))\<rbrakk> \<Longrightarrow> cur_thread x2 = idle_thread x2
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> (silc_inv (current_aag x2) s0_internal and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject (current_aag x2) (cur_thread s))) x2a
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag x2) x2 x2a
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 5. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> (silc_inv (current_aag x2) s0_internal and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject (current_aag x2) (cur_thread s))) x2a
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag x2) x2 x2a
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (4 subgoals):
 1. \<And>x1 x1a x2 x1b x2a ab bba ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; snd s' = f (if ct_running bba then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; (ab, bba) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bba then InUserMode else InIdleMode); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bba); fst t' = (ac, bc); invs x2; invs x2a; invs bba; invs bc; valid_list x2; valid_list x2a; valid_list bba; valid_list bc; valid_sched_2 (ready_queues x2) (ekheap x2) resume_cur_thread (cur_domain x2) (kheap x2) (cur_thread x2) (idle_thread x2); valid_sched_2 (ready_queues x2a) (ekheap x2a) resume_cur_thread (cur_domain x2a) (kheap x2a) (cur_thread x2a) (idle_thread x2a); valid_sched bba; valid_sched bc; only_timer_irq_inv timer_irq s0_internal x2; only_timer_irq_inv timer_irq s0_internal x2a; only_timer_irq_inv timer_irq s0_internal bba; only_timer_irq_inv timer_irq s0_internal bc; silc_inv (current_aag x2) s0_internal x2; silc_inv (current_aag x2a) s0_internal x2a; silc_inv (current_aag bba) s0_internal bba; silc_inv (current_aag bc) s0_internal bc; domain_sep_inv False s0_internal x2; domain_sep_inv False s0_internal x2a; domain_sep_inv False s0_internal bba; domain_sep_inv False s0_internal bc; pas_refined (current_aag x2) x2; pas_refined (current_aag x2a) x2a; pas_refined (current_aag bba) bba; pas_refined (current_aag bc) bc; guarded_pas_domain (current_aag x2) x2; guarded_pas_domain (current_aag x2a) x2a; guarded_pas_domain (current_aag bba) bba; guarded_pas_domain (current_aag bc) bc; idle_equiv s0_internal x2; idle_equiv s0_internal x2a; idle_equiv s0_internal bba; idle_equiv s0_internal bc; valid_domain_list x2; valid_domain_list x2a; valid_domain_list bba; valid_domain_list bc; valid_vspace_objs_if x2; valid_vspace_objs_if x2a; valid_vspace_objs_if bba; valid_vspace_objs_if bc; det_inv KernelExit (cur_thread_context_of ((x1a, x2), KernelExit)) x2; det_inv KernelExit (cur_thread_context_of ((x1b, x2a), KernelExit)) x2a; det_inv (sys_mode_of s') (cur_thread_context_of s') bba; det_inv (sys_mode_of t') (cur_thread_context_of t') bc; 0 < domain_time x2; 0 < domain_time x2a; f (if ct_running bba then InUserMode else InIdleMode) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time bba; f (if ct_running bc then InUserMode else InIdleMode) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time bc; domain_time x2 \<noteq> 0; domain_time x2a \<noteq> 0; domain_time bba = 0 \<longrightarrow> scheduler_action bba = choose_new_thread; domain_time bc = 0 \<longrightarrow> scheduler_action bc = choose_new_thread; ct_running x2 \<or> ct_idle x2; scheduler_action x2 = resume_cur_thread; ct_running x2a \<or> ct_idle x2a; scheduler_action x2a = resume_cur_thread; f (if ct_running bba then InUserMode else InIdleMode) \<noteq> KernelExit \<longrightarrow> ct_idle bba \<longrightarrow> user_context_of s' = idle_context bba; case f (if ct_running bba then InUserMode else InIdleMode) 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 (if ct_running bc then InUserMode else InIdleMode) \<noteq> KernelExit \<longrightarrow> ct_idle bc \<longrightarrow> user_context_of t' = idle_context bc; case f (if ct_running bc then InUserMode else InIdleMode) 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\<rbrakk> \<Longrightarrow> silc_inv (current_aag x2) s0_internal x2a \<and> (cur_thread x2a = idle_thread x2a \<or> is_subject (current_aag x2) (cur_thread x2a))
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag x2) x2 x2a
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (4 subgoals):
 1. \<And>x1 x1a x2 x1b x2a ab bba ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; snd s' = f (if ct_running bba then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; (ab, bba) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bba then InUserMode else InIdleMode); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bba); fst t' = (ac, bc); invs x2; invs x2a; invs bba; invs bc; valid_list x2; valid_list x2a; valid_list bba; valid_list bc; valid_sched_2 (ready_queues x2) (ekheap x2) resume_cur_thread (cur_domain x2) (kheap x2) (cur_thread x2) (idle_thread x2); valid_sched_2 (ready_queues x2a) (ekheap x2a) resume_cur_thread (cur_domain x2a) (kheap x2a) (cur_thread x2a) (idle_thread x2a); valid_sched bba; valid_sched bc; only_timer_irq_inv timer_irq s0_internal x2; only_timer_irq_inv timer_irq s0_internal x2a; only_timer_irq_inv timer_irq s0_internal bba; only_timer_irq_inv timer_irq s0_internal bc; silc_inv (current_aag x2) s0_internal x2; silc_inv (current_aag x2a) s0_internal x2a; silc_inv (current_aag bba) s0_internal bba; silc_inv (current_aag bc) s0_internal bc; domain_sep_inv False s0_internal x2; domain_sep_inv False s0_internal x2a; domain_sep_inv False s0_internal bba; domain_sep_inv False s0_internal bc; pas_refined (current_aag x2) x2; pas_refined (current_aag x2a) x2a; pas_refined (current_aag bba) bba; pas_refined (current_aag bc) bc; guarded_pas_domain (current_aag x2) x2; guarded_pas_domain (current_aag x2a) x2a; guarded_pas_domain (current_aag bba) bba; guarded_pas_domain (current_aag bc) bc; idle_equiv s0_internal x2; idle_equiv s0_internal x2a; idle_equiv s0_internal bba; idle_equiv s0_internal bc; valid_domain_list x2; valid_domain_list x2a; valid_domain_list bba; valid_domain_list bc; valid_vspace_objs_if x2; valid_vspace_objs_if x2a; valid_vspace_objs_if bba; valid_vspace_objs_if bc; det_inv KernelExit (cur_thread_context_of ((x1a, x2), KernelExit)) x2; det_inv KernelExit (cur_thread_context_of ((x1b, x2a), KernelExit)) x2a; det_inv (sys_mode_of s') (cur_thread_context_of s') bba; det_inv (sys_mode_of t') (cur_thread_context_of t') bc; 0 < domain_time x2; 0 < domain_time x2a; f (if ct_running bba then InUserMode else InIdleMode) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time bba; f (if ct_running bc then InUserMode else InIdleMode) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time bc; domain_time x2 \<noteq> 0; domain_time x2a \<noteq> 0; domain_time bba = 0 \<longrightarrow> scheduler_action bba = choose_new_thread; domain_time bc = 0 \<longrightarrow> scheduler_action bc = choose_new_thread; ct_running x2 \<or> ct_idle x2; scheduler_action x2 = resume_cur_thread; ct_running x2a \<or> ct_idle x2a; scheduler_action x2a = resume_cur_thread; f (if ct_running bba then InUserMode else InIdleMode) \<noteq> KernelExit \<longrightarrow> ct_idle bba \<longrightarrow> user_context_of s' = idle_context bba; case f (if ct_running bba then InUserMode else InIdleMode) 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 (if ct_running bc then InUserMode else InIdleMode) \<noteq> KernelExit \<longrightarrow> ct_idle bc \<longrightarrow> user_context_of t' = idle_context bc; case f (if ct_running bc then InUserMode else InIdleMode) 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; cur_domain (internal_state_if ((x1a, x2), KernelExit)) = cur_domain (internal_state_if ((x1b, x2a), KernelExit))\<rbrakk> \<Longrightarrow> silc_inv (current_aag x2) s0_internal x2a \<and> (cur_thread x2a = idle_thread x2a \<or> is_subject (current_aag x2) (cur_thread x2a))
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag x2) x2 x2a
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (4 subgoals):
 1. \<And>x1 x1a x2 x1b x2a ab bba ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; snd s' = f (if ct_running bba then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rparr>) x2 x2a; affects_equiv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rparr>) (OrdinaryLabel x1) x2 x2a; (ab, bba) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bba then InUserMode else InIdleMode); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bba); fst t' = (ac, bc); invs x2; invs x2a; invs bba; invs bc; valid_list x2; valid_list x2a; valid_list bba; valid_list bc; valid_sched_2 (ready_queues x2) (ekheap x2) resume_cur_thread (cur_domain x2a) (kheap x2) (cur_thread x2) (idle_thread x2); valid_sched_2 (ready_queues x2a) (ekheap x2a) resume_cur_thread (cur_domain x2a) (kheap x2a) (cur_thread x2a) (idle_thread x2a); valid_sched bba; valid_sched bc; only_timer_irq_inv timer_irq s0_internal x2; only_timer_irq_inv timer_irq s0_internal x2a; only_timer_irq_inv timer_irq s0_internal bba; only_timer_irq_inv timer_irq s0_internal bc; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rparr>) s0_internal x2; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rparr>) s0_internal x2a; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bba))\<rparr>) s0_internal bba; silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bc))\<rparr>) s0_internal bc; domain_sep_inv False s0_internal x2; domain_sep_inv False s0_internal x2a; domain_sep_inv False s0_internal bba; domain_sep_inv False s0_internal bc; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rparr>) x2; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rparr>) x2a; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bba))\<rparr>) bba; pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain bc))\<rparr>) bc; cur_thread x2 \<noteq> idle_thread x2 \<longrightarrow> pasObjectAbs initial_aag (cur_thread x2) \<in> pasDomainAbs initial_aag (cur_domain x2a); cur_thread x2a \<noteq> idle_thread x2a \<longrightarrow> pasObjectAbs initial_aag (cur_thread x2a) \<in> pasDomainAbs initial_aag (cur_domain x2a); cur_thread bba \<noteq> idle_thread bba \<longrightarrow> pasObjectAbs initial_aag (cur_thread bba) \<in> pasDomainAbs initial_aag (cur_domain bba); cur_thread bc \<noteq> idle_thread bc \<longrightarrow> pasObjectAbs initial_aag (cur_thread bc) \<in> pasDomainAbs initial_aag (cur_domain bc); idle_equiv s0_internal x2; idle_equiv s0_internal x2a; idle_equiv s0_internal bba; idle_equiv s0_internal bc; valid_domain_list x2; valid_domain_list x2a; valid_domain_list bba; valid_domain_list bc; valid_vspace_objs_if x2; valid_vspace_objs_if x2a; valid_vspace_objs_if bba; valid_vspace_objs_if bc; det_inv KernelExit (cur_thread_context_of ((x1a, x2), KernelExit)) x2; det_inv KernelExit (cur_thread_context_of ((x1b, x2a), KernelExit)) x2a; det_inv (sys_mode_of s') (cur_thread_context_of s') bba; det_inv (sys_mode_of t') (cur_thread_context_of t') bc; 0 < domain_time x2; 0 < domain_time x2a; f (if ct_running bba then InUserMode else InIdleMode) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time bba; f (if ct_running bc then InUserMode else InIdleMode) \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time bc; domain_time x2 \<noteq> 0; domain_time x2a \<noteq> 0; domain_time bba = 0 \<longrightarrow> scheduler_action bba = choose_new_thread; domain_time bc = 0 \<longrightarrow> scheduler_action bc = choose_new_thread; ct_running x2 \<or> ct_idle x2; scheduler_action x2 = resume_cur_thread; ct_running x2a \<or> ct_idle x2a; scheduler_action x2a = resume_cur_thread; f (if ct_running bba then InUserMode else InIdleMode) \<noteq> KernelExit \<longrightarrow> ct_idle bba \<longrightarrow> user_context_of s' = idle_context bba; case f (if ct_running bba then InUserMode else InIdleMode) 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 (if ct_running bc then InUserMode else InIdleMode) \<noteq> KernelExit \<longrightarrow> ct_idle bc \<longrightarrow> user_context_of t' = idle_context bc; case f (if ct_running bc then InUserMode else InIdleMode) 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; cur_domain x2 = cur_domain x2a; pasObjectAbs initial_aag (cur_thread x2a) \<noteq> the_elem (pasDomainAbs initial_aag (cur_domain x2a))\<rbrakk> \<Longrightarrow> cur_thread x2a = idle_thread x2a
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag x2) x2 x2a
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag x2) x2 x2a
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc)\<rbrakk> \<Longrightarrow> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) x2 x2a
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (?l47 a b aa ba x1 x1a x2 x1b x2a ab bb ac bc) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb ac bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ac, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ac, bc); ab = ac \<and> reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ab, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc \<and> affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); (ab, bb) \<in> fst (kernel_exit_if x1a x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); (ab, bc) \<in> fst (kernel_exit_if x1b x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t')) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> (ct_running bb \<longrightarrow> (ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t') \<and> ct_running bc) \<and> (\<not> ct_running bb \<longrightarrow> \<not> ct_running bc \<and> (\<not> ct_running bc \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, x2), KernelExit)) t'))
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((x1a, bb), KernelExit)) t'
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (11 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag (internal_state_if ((x1a, bb), KernelExit))) (internal_state_if s') (internal_state_if t')
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> affects_equiv (current_aag (internal_state_if ((x1a, bb), KernelExit))) (OrdinaryLabel x1) (internal_state_if s') (internal_state_if t')
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> policy2 (part ((x1a, bb), KernelExit)) (Partition x1)
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> part ((x1a, bb), KernelExit) \<noteq> PSched
 5. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s')
 6. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> uwr2 ((x1a, bb), KernelExit) PSched (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc)
 7. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((x1a, bb), KernelExit))) (internal_state_if ((x1a, bb), KernelExit)) (internal_state_if s')
 8. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc))) (internal_state_if (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc)) (internal_state_if t')
 9. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 10. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
A total of 11 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> silc_inv (current_aag bb) s0_internal bb
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> uwr2 ((x1a, bb), KernelExit) PSched (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc)
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((x1a, bb), KernelExit))) (internal_state_if ((x1a, bb), KernelExit)) (internal_state_if s')
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc))) (internal_state_if (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc)) (internal_state_if t')
 5. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 6. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
 7. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> uwr2 ((x1a, bb), KernelExit) PSched (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc)
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((x1a, bb), KernelExit))) (internal_state_if ((x1a, bb), KernelExit)) (internal_state_if s')
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc))) (internal_state_if (?t223 a b aa ba x1 x1a x2 x1b x2a ab bb bc)) (internal_state_if t')
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 5. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
 6. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((x1a, bb), KernelExit))) (internal_state_if ((x1a, bb), KernelExit)) (internal_state_if s')
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (aa, ba))) (internal_state_if (aa, ba)) (internal_state_if t')
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
 5. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag bb) bb bb
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (aa, ba))) (internal_state_if (aa, ba)) (internal_state_if t')
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
 5. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (aa, ba))) (internal_state_if (aa, ba)) (internal_state_if t')
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag bc) bc bc
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, bb), KernelExit); t = ((x1b, bc), KernelExit); u = Partition x1; uwr2 ((x1a, bb), KernelExit) PSched ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (part ((x1a, bb), KernelExit)) ((x1b, bc), KernelExit); uwr2 ((x1a, bb), KernelExit) (Partition x1) ((x1b, bc), KernelExit); invs_if ((x1a, bb), KernelExit); invs_if ((x1b, bc), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, bb), KernelExit)) (Partition x1); part ((x1a, bb), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bc then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag bb) bb bc; affects_equiv (current_aag bb) (OrdinaryLabel x1) bb bc; a = (x1a, bb); x = (if ct_running bc then InUserMode else InIdleMode); aa = (x1b, bc); fst s' = (ab, bb); fst t' = (ab, bc); x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t'
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> Invs bb
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> Invs bc
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> current_aag x2 = current_aag bb
 4. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> Invs bc
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> current_aag x2 = current_aag bb
 3. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc\<rbrakk> \<Longrightarrow> current_aag x2 = current_aag bb
 2. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x1 x1a x2 x1b x2a ab bb bc. \<lbrakk>y = (if ct_running bc then InUserMode else InIdleMode); s = ((x1a, x2), KernelExit); t = ((x1b, x2a), KernelExit); u = Partition x1; uwr2 ((x1a, x2), KernelExit) PSched ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (part ((x1a, x2), KernelExit)) ((x1b, x2a), KernelExit); uwr2 ((x1a, x2), KernelExit) (Partition x1) ((x1b, x2a), KernelExit); invs_if ((x1a, x2), KernelExit); invs_if ((x1b, x2a), KernelExit); invs_if s'; invs_if t'; policy2 (part ((x1a, x2), KernelExit)) (Partition x1); part ((x1a, x2), KernelExit) \<noteq> PSched; b = KernelExit; ba = KernelExit; snd s' = f (if ct_running bb then InUserMode else InIdleMode); snd t' = f (if ct_running bc then InUserMode else InIdleMode); reads_equiv_f_g (current_aag x2) x2 x2a; affects_equiv (current_aag x2) (OrdinaryLabel x1) x2 x2a; a = (x1a, x2); x = (if ct_running bb then InUserMode else InIdleMode); aa = (x1b, x2a); fst s' = (ab, bb); fst t' = (ab, bc); reads_equiv_f_g (current_aag x2) bb bc; affects_equiv (current_aag x2) (OrdinaryLabel x1) bb bc; x2 = bb; x2a = bc; ct_running bb = ct_running bc\<rbrakk> \<Longrightarrow> ct_running bb = ct_running bc proof (prove)
goal:
No subgoals!