theory Noninterference

lemma check_active_irq_A_if_confidentiality_helper:
  notes reads_respects_irq = use_ev[OF check_active_irq_if_reads_respects_f_g[where st=s0_internal
                                                                                and st'=s0_internal
                                                                                and irq=timer_irq]]
  shows
    "\<lbrakk> (s, t) \<in> uwr PSched; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u; invs_if s; invs_if t;
       silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s');
       (part s, u) \<in> policyFlows (pasPolicy initial_aag);
       part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s);
       ((fst s),x,(fst s')) \<in> check_active_irq_A_if; ((fst t),y,(fst t')) \<in> check_active_irq_A_if \<rbrakk>
       \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y
                    \<longrightarrow> (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s))" apply (frule (1) uwr_part_sys_mode_of_user_context_of_eq) apply (clarsimp simp: check_active_irq_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 (match premises in "s = ((_, p), _)" and "t = ((_, q), _)"
                    and H: "(_, _) \<in> fst (check_active_irq_if _ p)"
                    for p q \<Rightarrow> \<open>rule revcut_rl[OF reads_respects_irq[where s=p and t=q, OF H]]\<close>) apply assumption apply (simp add: invs_if_def Invs_def) apply (elim conjE) apply assumption apply (simp add: invs_if_def Invs_def) apply (simp only: current_aag_eqI[OF uwr_PSched_cur_domain']) apply simp apply fastforce apply simp apply (rule impI) apply (rule reads_equiv_f_g_affects_equiv_uwr) apply simp+ apply (erule use_valid[OF _ check_active_irq_if_partitionIntegrity]) apply (rule partitionIntegrity_refl) apply simp apply (erule use_valid[OF _ check_active_irq_if_partitionIntegrity]) apply (rule partitionIntegrity_refl) apply (simp add: sys_mode_of_def) apply (simp add: user_context_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s); (fst s, x, fst s') \<in> check_active_irq_A_if; (fst t, y, fst t') \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> 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; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s'); policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s); (fst s, x, fst s') \<in> check_active_irq_A_if; (fst t, y, fst t') \<in> check_active_irq_A_if; sys_mode_of s = sys_mode_of t \<and> (user_modes (sys_mode_of s) \<longrightarrow> user_context_of s = user_context_of t)\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t') proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb xc yc. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; silc_inv (current_aag yb) s0_internal yb; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of t); fst s = (xa, ya); fst t = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); sys_mode_of s = sys_mode_of t; user_context_of s = user_context_of t\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t') proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) u ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) u; part ((xaa, ya), ba) \<noteq> PSched; u \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba)\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (6 subgoals):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> (?rv'20 xa ya xaa yaa xb yb xc yc a b aa ba x1, ?t'20 xa ya xaa yaa xb yb xc yc a b aa ba x1) \<in> fst (check_active_irq_if xaa yaa)
 2. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> (silc_inv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) s0_internal and invs and only_timer_irq_inv timer_irq s0_internal) ya
 3. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> (silc_inv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) s0_internal and invs and only_timer_irq_inv timer_irq s0_internal) yaa
 4. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 5. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> affects_equiv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 6. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); ?rv'20 xa ya xaa yaa xb yb xc yc a b aa ba x1 = (x, xb) \<and> reads_equiv_f_g (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb (?t'20 xa ya xaa yaa xb yb xc yc a b aa ba x1) \<and> affects_equiv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb (?t'20 xa ya xaa yaa xb yb xc yc a b aa ba x1)\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (5 subgoals):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> (silc_inv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) s0_internal and invs and only_timer_irq_inv timer_irq s0_internal) ya
 2. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> (silc_inv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) s0_internal and invs and only_timer_irq_inv timer_irq s0_internal) yaa
 3. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 4. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> affects_equiv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 5. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); (y, xc) = (x, xb) \<and> reads_equiv_f_g (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc \<and> affects_equiv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (5 subgoals):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs ya \<and> valid_list ya \<and> valid_sched ya \<and> only_timer_irq_inv timer_irq s0_internal ya \<and> silc_inv (current_aag ya) s0_internal ya \<and> domain_sep_inv False s0_internal ya \<and> pas_refined (current_aag ya) ya \<and> guarded_pas_domain (current_aag ya) ya \<and> idle_equiv s0_internal ya \<and> valid_domain_list ya \<and> valid_vspace_objs_if ya \<and> det_inv ba (cur_thread_context_of ((xaa, ya), ba)) ya \<and> (ba \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time ya) \<and> (domain_time ya = 0 \<longrightarrow> scheduler_action ya = choose_new_thread) \<and> (ba \<noteq> KernelExit \<longrightarrow> ct_idle ya \<longrightarrow> xaa = idle_context ya) \<and> (case ba of InUserMode \<Rightarrow> ct_running (internal_state_if ((xaa, ya), ba)) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((xaa, ya), ba)) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((xaa, ya), ba))) \<and> (ct_running (internal_state_if ((xaa, ya), ba)) \<or> ct_idle (internal_state_if ((xaa, ya), ba))) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((xaa, ya), ba)) \<or> ct_idle (internal_state_if ((xaa, ya), ba))) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | _ \<Rightarrow> True); invs yaa \<and> valid_list yaa \<and> valid_sched yaa \<and> only_timer_irq_inv timer_irq s0_internal yaa \<and> silc_inv (current_aag yaa) s0_internal yaa \<and> domain_sep_inv False s0_internal yaa \<and> pas_refined (current_aag yaa) yaa \<and> guarded_pas_domain (current_aag yaa) yaa \<and> idle_equiv s0_internal yaa \<and> valid_domain_list yaa \<and> valid_vspace_objs_if yaa \<and> det_inv ba (cur_thread_context_of ((xaa, yaa), ba)) yaa \<and> (ba \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time yaa) \<and> (domain_time yaa = 0 \<longrightarrow> scheduler_action yaa = choose_new_thread) \<and> (ba \<noteq> KernelExit \<longrightarrow> ct_idle yaa \<longrightarrow> xaa = idle_context yaa) \<and> (case ba of InUserMode \<Rightarrow> ct_running (internal_state_if ((xaa, yaa), ba)) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((xaa, yaa), ba)) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((xaa, yaa), ba))) \<and> (ct_running (internal_state_if ((xaa, yaa), ba)) \<or> ct_idle (internal_state_if ((xaa, yaa), ba))) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((xaa, yaa), ba)) \<or> ct_idle (internal_state_if ((xaa, yaa), ba))) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | _ \<Rightarrow> True); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa\<rbrakk> \<Longrightarrow> silc_inv (?aag21 xaa ya xaa yaa xb yb xc yc (xaa, ya) ba (xaa, yaa) ba x1) s0_internal ya
 2. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> (silc_inv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) s0_internal and invs and only_timer_irq_inv timer_irq s0_internal) yaa
 3. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 4. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> affects_equiv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 5. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); (y, xc) = (x, xb) \<and> reads_equiv_f_g (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc \<and> affects_equiv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (5 subgoals):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; invs ya; invs yaa; reads_equiv_f_g (current_aag ya) ya yaa; affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; valid_list ya; valid_list yaa; valid_sched ya; valid_sched yaa; only_timer_irq_inv timer_irq s0_internal ya; only_timer_irq_inv timer_irq s0_internal yaa; silc_inv (current_aag ya) s0_internal ya; silc_inv (current_aag yaa) s0_internal yaa; domain_sep_inv False s0_internal ya; domain_sep_inv False s0_internal yaa; pas_refined (current_aag ya) ya; pas_refined (current_aag yaa) yaa; guarded_pas_domain (current_aag ya) ya; guarded_pas_domain (current_aag yaa) yaa; idle_equiv s0_internal ya; idle_equiv s0_internal yaa; valid_domain_list ya; valid_domain_list yaa; valid_vspace_objs_if ya; valid_vspace_objs_if yaa; det_inv ba (cur_thread_context_of ((xaa, ya), ba)) ya; det_inv ba (cur_thread_context_of ((xaa, yaa), ba)) yaa; ba \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time ya; ba \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time yaa; domain_time ya = 0 \<longrightarrow> scheduler_action ya = choose_new_thread; domain_time yaa = 0 \<longrightarrow> scheduler_action yaa = choose_new_thread; ba \<noteq> KernelExit \<longrightarrow> ct_idle ya \<longrightarrow> xaa = idle_context ya; case ba of InUserMode \<Rightarrow> ct_running (internal_state_if ((xaa, ya), ba)) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((xaa, ya), ba)) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((xaa, ya), ba))) \<and> (ct_running (internal_state_if ((xaa, ya), ba)) \<or> ct_idle (internal_state_if ((xaa, ya), ba))) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((xaa, ya), ba)) \<or> ct_idle (internal_state_if ((xaa, ya), ba))) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | _ \<Rightarrow> True; ba \<noteq> KernelExit \<longrightarrow> ct_idle yaa \<longrightarrow> xaa = idle_context yaa; case ba of InUserMode \<Rightarrow> ct_running (internal_state_if ((xaa, yaa), ba)) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((xaa, yaa), ba)) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((xaa, yaa), ba))) \<and> (ct_running (internal_state_if ((xaa, yaa), ba)) \<or> ct_idle (internal_state_if ((xaa, yaa), ba))) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((xaa, yaa), ba)) \<or> ct_idle (internal_state_if ((xaa, yaa), ba))) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> silc_inv (?aag21 xaa ya xaa yaa xb yb xc yc (xaa, ya) ba (xaa, yaa) ba x1) s0_internal ya
 2. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> (silc_inv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) s0_internal and invs and only_timer_irq_inv timer_irq s0_internal) yaa
 3. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 4. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> affects_equiv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 5. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); (y, xc) = (x, xb) \<and> reads_equiv_f_g (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc \<and> affects_equiv (?aag21 xa ya xaa yaa xb yb xc yc a b aa ba x1) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (4 subgoals):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> (silc_inv (current_aag ya) s0_internal and invs and only_timer_irq_inv timer_irq s0_internal) yaa
 2. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag ya) ya yaa
 3. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag ya) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 4. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); (y, xc) = (x, xb) \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (4 subgoals):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs ya \<and> valid_list ya \<and> valid_sched ya \<and> only_timer_irq_inv timer_irq s0_internal ya \<and> silc_inv (current_aag ya) s0_internal ya \<and> domain_sep_inv False s0_internal ya \<and> pas_refined (current_aag ya) ya \<and> guarded_pas_domain (current_aag ya) ya \<and> idle_equiv s0_internal ya \<and> valid_domain_list ya \<and> valid_vspace_objs_if ya \<and> det_inv ba (cur_thread_context_of ((xaa, ya), ba)) ya \<and> (ba \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time ya) \<and> (domain_time ya = 0 \<longrightarrow> scheduler_action ya = choose_new_thread) \<and> (ba \<noteq> KernelExit \<longrightarrow> ct_idle ya \<longrightarrow> xaa = idle_context ya) \<and> (case ba of InUserMode \<Rightarrow> ct_running (internal_state_if ((xaa, ya), ba)) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((xaa, ya), ba)) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((xaa, ya), ba))) \<and> (ct_running (internal_state_if ((xaa, ya), ba)) \<or> ct_idle (internal_state_if ((xaa, ya), ba))) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((xaa, ya), ba)) \<or> ct_idle (internal_state_if ((xaa, ya), ba))) \<and> scheduler_action (internal_state_if ((xaa, ya), ba)) = resume_cur_thread | _ \<Rightarrow> True); invs yaa \<and> valid_list yaa \<and> valid_sched yaa \<and> only_timer_irq_inv timer_irq s0_internal yaa \<and> silc_inv (current_aag yaa) s0_internal yaa \<and> domain_sep_inv False s0_internal yaa \<and> pas_refined (current_aag yaa) yaa \<and> guarded_pas_domain (current_aag yaa) yaa \<and> idle_equiv s0_internal yaa \<and> valid_domain_list yaa \<and> valid_vspace_objs_if yaa \<and> det_inv ba (cur_thread_context_of ((xaa, yaa), ba)) yaa \<and> (ba \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time yaa) \<and> (domain_time yaa = 0 \<longrightarrow> scheduler_action yaa = choose_new_thread) \<and> (ba \<noteq> KernelExit \<longrightarrow> ct_idle yaa \<longrightarrow> xaa = idle_context yaa) \<and> (case ba of InUserMode \<Rightarrow> ct_running (internal_state_if ((xaa, yaa), ba)) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((xaa, yaa), ba)) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((xaa, yaa), ba))) \<and> (ct_running (internal_state_if ((xaa, yaa), ba)) \<or> ct_idle (internal_state_if ((xaa, yaa), ba))) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((xaa, yaa), ba)) \<or> ct_idle (internal_state_if ((xaa, yaa), ba))) \<and> scheduler_action (internal_state_if ((xaa, yaa), ba)) = resume_cur_thread | _ \<Rightarrow> True); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa\<rbrakk> \<Longrightarrow> silc_inv (current_aag ya) s0_internal yaa
 2. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag ya) ya yaa
 3. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag ya) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 4. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); (y, xc) = (x, xb) \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (3 subgoals):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag ya) ya yaa
 2. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag ya) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 3. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); (y, xc) = (x, xb) \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (2 subgoals):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba))\<rbrakk> \<Longrightarrow> affects_equiv (current_aag ya) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) ya yaa
 2. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); (y, xc) = (x, xb) \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (?l21 xa ya xaa yaa xb yb xc yc a b aa ba x1) yb yc\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb xc yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xc, yc); ((y, xc), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)) \<and> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if ((xaa, ya), ba)) (internal_state_if ((xaa, yaa), ba)); (y, xc) = (x, xb) \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t') proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc\<rbrakk> \<Longrightarrow> snd s' = f x \<and> snd t' = f x \<longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t' proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> uwr2 s' (Partition x1) t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part ((xaa, ya), ba)) t' proof (prove)
goal (10 subgoals):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if s') (internal_state_if t')
 2. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> affects_equiv (current_aag (internal_state_if ((xaa, ya), ba))) (OrdinaryLabel x1) (internal_state_if s') (internal_state_if t')
 3. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> policy2 (part ((xaa, ya), ba)) (Partition x1)
 4. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> part ((xaa, ya), ba) \<noteq> PSched
 5. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s')
 6. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> uwr2 ((xaa, ya), ba) PSched (?t74 xa ya xaa yaa xb yb yc a b aa ba x1)
 7. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if ((xaa, ya), ba))) (internal_state_if ((xaa, ya), ba)) (internal_state_if s')
 8. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (?t74 xa ya xaa yaa xb yb yc a b aa ba x1))) (internal_state_if (?t74 xa ya xaa yaa xb yb yc a b aa ba x1)) (internal_state_if t')
 9. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 10. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag ya) ya yb
 2. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (aa, ba))) (internal_state_if (aa, ba)) (internal_state_if t')
 3. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (4 subgoals):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag ya) ya ya
 2. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (aa, ba))) (internal_state_if (aa, ba)) (internal_state_if t')
 3. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 4. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if (aa, ba))) (internal_state_if (aa, ba)) (internal_state_if t')
 2. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag yaa) yaa yc
 2. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (3 subgoals):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag yaa) yaa yaa
 2. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 3. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (2 subgoals):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> sys_mode_of s' = sys_mode_of t'
 2. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xaa yaa xb yb yc a b aa ba x1. \<lbrakk>uwr2 ((xaa, ya), ba) PSched ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (part ((xaa, ya), ba)) ((xaa, yaa), ba); uwr2 ((xaa, ya), ba) (Partition x1) ((xaa, yaa), ba); invs_if ((xaa, ya), ba); invs_if ((xaa, yaa), ba); silc_inv (current_aag yb) s0_internal yb; policy2 (part ((xaa, ya), ba)) (Partition x1); part ((xaa, ya), ba) \<noteq> PSched; user_modes ba; a = (xaa, ya); aa = (xaa, yaa); fst s' = (xb, yb); ((x, xb), yb) \<in> fst (check_active_irq_if xaa ya); fst t' = (xb, yc); ((x, xb), yc) \<in> fst (check_active_irq_if xaa yaa); b = ba; xa = xaa; s = ((xaa, ya), ba); t = ((xaa, yaa), ba); u = Partition x1; reads_equiv_f_g (current_aag ya) ya yaa \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) ya yaa; y = x \<and> reads_equiv_f_g (current_aag ya) yb yc \<and> affects_equiv (current_aag ya) (OrdinaryLabel x1) yb yc; snd s' = f x \<and> snd t' = f x\<rbrakk> \<Longrightarrow> user_context_of s' = user_context_of t' proof (prove)
goal:
No subgoals!