theory Noninterference

lemma small_Step_confidentiality_part_not_PSched:
  shows
  "\<lbrakk>(s, s') \<in> Simulation.Step (ADT_A_if utf) ();
    (t, t') \<in> Simulation.Step (ADT_A_if utf) ();
    (s, t) \<in> uwr PSched; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u;
    system.reachable (ADT_A_if utf) s0 s;
    system.reachable (ADT_A_if utf) s0 t;
    (part s, u) \<in> policyFlows (pasPolicy initial_aag);
    part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow>
   (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s)" apply (frule schedIncludesCurrentDom) apply (frule uwr_part_sys_mode_of_eq, simp+) apply (frule_tac s=s in ADT_A_if_reachable_invs_if) apply (frule_tac s=t in ADT_A_if_reachable_invs_if) apply (frule(2) Step_system.reachable_Step[where s=s, OF ADT_A_if_Step_system _ Step_ADT_A_if'']) apply (frule(2) Step_system.reachable_Step[where s=t, OF ADT_A_if_Step_system _ Step_ADT_A_if'']) apply (frule_tac s=s' in ADT_A_if_reachable_invs_if) apply (frule_tac s=t' in ADT_A_if_reachable_invs_if) apply (case_tac "sys_mode_of s") 
       (* InUserMode *)
        apply ((simp add: Step_ADT_A_if_def_global_automaton_if global_automaton_if_def
                 split: if_splits
              | intro impI allI
              | elim exE conjE disjE
              | simp_all add: not_schedule_modes_KernelEntry)+)[1] apply (drule do_user_op_A_if_confidentiality'[
                                     where s=s and t=t and s'=s' and t'=t' and u=u],simp+) apply (drule do_user_op_A_if_confidentiality'[
                                  where s=s and t=t and s'=s' and t'=t' and u=u], simp+) apply (drule_tac s=s and t=t and u=u and s'="(aa,ba)"
                          in check_active_irq_A_if_retval_eq, simp+) apply (drule do_user_op_A_if_confidentiality'[
                                where s=s and t=t and s'=s' and t'=t' and u=u], simp+) apply (drule_tac s=s and t=t and u=u and s'="(ad,bd)"
                        in check_active_irq_A_if_retval_eq, simp+) apply (drule do_user_op_A_if_confidentiality'[
                                where s=s and t=t and s'=s' and t'=t' and u=u], simp+) apply (drule_tac s=s and t=t and u=u and s'="(aa,ba)"
                      in check_active_irq_A_if_retval_eq, simp+) apply (drule_tac s=s and t=t and u=u and s'="(ad,bd)"
                    in check_active_irq_A_if_retval_eq, simp+) apply (drule check_active_irq_A_if_confidentiality'[
                            where s=s and t=t and s'=s' and t'=t' and u=u], simp+) 
      (* InIdleMode *)
       apply ((simp add: Step_ADT_A_if_def_global_automaton_if global_automaton_if_def
                  split: if_splits
             | intro impI allI
             | elim exE conjE disjE
             | simp_all add: not_schedule_modes_KernelEntry)+)[1] apply (drule check_active_irq_A_if_confidentiality'[
                                      where s=s and t=t and s'=s' and t'=t' and u=u], simp+) apply (drule_tac s=s and t=t and u=u and s'="(aa,ba)" in check_active_irq_A_if_retval_eq,
              simp+) apply (drule_tac s=s and t=t and u=u and s'="(aa,ba)" in check_active_irq_A_if_retval_eq,
             simp+) apply (drule check_active_irq_A_if_confidentiality''[
                          where s=s and t=t and s'=s' and t'=t' and u=u],simp+) 
     (* KernelEntry event -- where event \<noteq> Interrupt *)
      apply (rename_tac event) apply (subgoal_tac "event \<noteq> Interrupt") prefer 2 apply (case_tac t, simp) apply (case_tac event, (fastforce simp: part_def split: if_splits)+)[1] apply ((simp add: Step_ADT_A_if_def_global_automaton_if global_automaton_if_def
                 split: if_splits
            | intro impI allI
            | elim exE conjE disjE
            | simp_all add: not_schedule_modes_KernelEntry)+)[1] apply (drule kernel_call_A_if_confidentiality'[where s=s and t=t and s'=s' and t'=t' and u=u],
              simp+) apply (drule kernel_call_A_if_confidentiality'[where s=s and t=t and s'=s' and t'=t' and u=u],
             simp+) apply (drule kernel_call_A_if_confidentiality'[where s=s and t=t and s'=s' and t'=t' and u=u],
            simp+) apply (drule kernel_call_A_if_confidentiality'[where s=s and t=t and s'=s' and t'=t' and u=u],
           simp+) 
    (* KernelPreempted *)
     apply (simp add: part_def) 
    (* KernelSchedule bool -- where \<not> bool *)
    apply ((simp add: Step_ADT_A_if_def_global_automaton_if global_automaton_if_def
               split: if_splits
         | intro impI allI
         | elim exE conjE disjE
         | simp_all add: not_schedule_modes_KernelEntry)+)[1] apply (drule kernel_schedule_if_confidentiality'[where s=s and t=t and s'=s' and t'=t' and u=u],
         simp+) 
  (* KernelExit *)
   apply ((simp add: Step_ADT_A_if_def_global_automaton_if global_automaton_if_def
              split: if_splits
        | intro impI allI
        | elim exE conjE disjE
        | simp_all add: not_schedule_modes_KernelEntry)+)[1] apply (drule kernel_exit_A_if_confidentiality'[where s=s and t=t and s'=s' and t'=t' and u=u],
        simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; part s = part t\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InUserMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InUserMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (14 subgoals):
 1. \<And>a b aa ba ab bb e ac bc ad bd ae be ea. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ae, be), KernelEntry ea); invs_if ((ab, bb), KernelEntry e); invs_if ((ae, be), KernelEntry ea); step_restrict ((ab, bb), KernelEntry e); step_restrict ((ae, be), KernelEntry ea); s = ((a, b), InUserMode); s' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; t = ((ac, bc), InUserMode); t' = ((ae, be), KernelEntry ea); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), Some ea, ae, be) \<in> do_user_op_A_if utf; ea \<noteq> Interrupt\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), KernelEntry e) u ((ae, be), KernelEntry ea) \<and> uwr2 ((ab, bb), KernelEntry e) PSched ((ae, be), KernelEntry ea) \<and> uwr2 ((ab, bb), KernelEntry e) (part ((ac, bc), InUserMode)) ((ae, be), KernelEntry ea)
 2. \<And>a b aa ba ab bb e ac bc ad bd ae be. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); invs_if ((ab, bb), KernelEntry e); invs_if ((ae, be), InUserMode); step_restrict ((ab, bb), KernelEntry e); step_restrict ((ae, be), InUserMode); s = ((a, b), InUserMode); s' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; t = ((ac, bc), InUserMode); t' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), KernelEntry e) u ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), KernelEntry e) PSched ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), KernelEntry e) (part ((ac, bc), InUserMode)) ((ae, be), InUserMode)
 3. \<And>a b aa ba ab bb e ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), KernelEntry e); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), KernelEntry e); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), KernelEntry e) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), KernelEntry e) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), KernelEntry e) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 4. \<And>a b aa ba ab bb e ac bc ad bd ae be. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ae, be), InUserMode); invs_if ((ab, bb), KernelEntry e); step_restrict ((ae, be), InUserMode); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ae, be), InUserMode) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ae, be), InUserMode) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ae, be), InUserMode) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 5. \<And>a b aa ba ab bb e ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), KernelEntry e); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 6. \<And>a b aa ba ab bb ac bc ad bd ae be. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); invs_if ((ab, bb), InUserMode); invs_if ((ae, be), InUserMode); step_restrict ((ab, bb), InUserMode); step_restrict ((ae, be), InUserMode); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ae, be), InUserMode)
 7. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 8. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); t = ((a, b), InUserMode); t' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), InUserMode)
 9. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 10. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>a b aa ba ab bb e ac bc ad bd ae be. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); invs_if ((ab, bb), KernelEntry e); invs_if ((ae, be), InUserMode); step_restrict ((ab, bb), KernelEntry e); step_restrict ((ae, be), InUserMode); s = ((a, b), InUserMode); s' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; t = ((ac, bc), InUserMode); t' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), KernelEntry e) u ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), KernelEntry e) PSched ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), KernelEntry e) (part ((ac, bc), InUserMode)) ((ae, be), InUserMode)
 2. \<And>a b aa ba ab bb e ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), KernelEntry e); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), KernelEntry e); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), KernelEntry e) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), KernelEntry e) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), KernelEntry e) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 3. \<And>a b aa ba ab bb e ac bc ad bd ae be. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ae, be), InUserMode); invs_if ((ab, bb), KernelEntry e); step_restrict ((ae, be), InUserMode); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ae, be), InUserMode) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ae, be), InUserMode) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ae, be), InUserMode) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 4. \<And>a b aa ba ab bb e ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), KernelEntry e); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 5. \<And>a b aa ba ab bb ac bc ad bd ae be. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); invs_if ((ab, bb), InUserMode); invs_if ((ae, be), InUserMode); step_restrict ((ab, bb), InUserMode); step_restrict ((ae, be), InUserMode); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ae, be), InUserMode)
 6. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 7. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); t = ((a, b), InUserMode); t' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), InUserMode)
 8. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 9. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 10. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a b aa ba ab bb e ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), KernelEntry e); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), KernelEntry e); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), KernelEntry e) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), KernelEntry e) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), KernelEntry e) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 2. \<And>a b aa ba ab bb e ac bc ad bd ae be. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ae, be), InUserMode); invs_if ((ab, bb), KernelEntry e); step_restrict ((ae, be), InUserMode); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ae, be), InUserMode) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ae, be), InUserMode) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ae, be), InUserMode) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 3. \<And>a b aa ba ab bb e ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), KernelEntry e); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 4. \<And>a b aa ba ab bb ac bc ad bd ae be. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); invs_if ((ab, bb), InUserMode); invs_if ((ae, be), InUserMode); step_restrict ((ab, bb), InUserMode); step_restrict ((ae, be), InUserMode); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ae, be), InUserMode)
 5. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 6. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); t = ((a, b), InUserMode); t' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), InUserMode)
 7. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 8. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 9. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 10. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a b aa ba ab bb e ac bc ad bd ae be. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ae, be), InUserMode); invs_if ((ab, bb), KernelEntry e); step_restrict ((ae, be), InUserMode); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ae, be), InUserMode) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ae, be), InUserMode) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ae, be), InUserMode) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 2. \<And>a b aa ba ab bb e ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), KernelEntry e); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 3. \<And>a b aa ba ab bb ac bc ad bd ae be. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); invs_if ((ab, bb), InUserMode); invs_if ((ae, be), InUserMode); step_restrict ((ab, bb), InUserMode); step_restrict ((ae, be), InUserMode); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ae, be), InUserMode)
 4. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 5. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); t = ((a, b), InUserMode); t' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), InUserMode)
 6. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 7. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 8. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 9. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 10. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>a b aa ba ab bb e ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), KernelEntry e); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), KernelEntry e); t = ((a, b), InUserMode); t' = ((ab, bb), KernelEntry e); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf; e \<noteq> Interrupt; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), KernelEntry e) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), KernelEntry e)
 2. \<And>a b aa ba ab bb ac bc ad bd ae be. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); invs_if ((ab, bb), InUserMode); invs_if ((ae, be), InUserMode); step_restrict ((ab, bb), InUserMode); step_restrict ((ae, be), InUserMode); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ae, be), InUserMode)
 3. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 4. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); t = ((a, b), InUserMode); t' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), InUserMode)
 5. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 6. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 7. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 8. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 9. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 10. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (9 subgoals):
 1. \<And>a b aa ba ab bb ac bc ad bd ae be. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ae, be), InUserMode); invs_if ((ab, bb), InUserMode); invs_if ((ae, be), InUserMode); step_restrict ((ab, bb), InUserMode); step_restrict ((ae, be), InUserMode); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ae, be), InUserMode); ((ac, bc), None, ad, bd) \<in> check_active_irq_A_if; ((ad, bd), None, ae, be) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ae, be), InUserMode) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ae, be), InUserMode)
 2. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 3. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); t = ((a, b), InUserMode); t' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), InUserMode)
 4. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 7. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 8. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 9. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (8 subgoals):
 1. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) (part ((ac, bc), InUserMode)) ((ac, bc), InUserMode); uwr2 ((a, b), InUserMode) u ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); policy2 (part ((ac, bc), InUserMode)) u; part ((ac, bc), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; t = ((ac, bc), InUserMode); t' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ab, bb), InUserMode) u ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) PSched ((ad, bd), KernelEntry Interrupt) \<and> uwr2 ((ab, bb), InUserMode) (part ((ac, bc), InUserMode)) ((ad, bd), KernelEntry Interrupt)
 2. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); t = ((a, b), InUserMode); t' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), InUserMode)
 3. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 7. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 8. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba ab bb ac bc ad bd i. \<lbrakk>uwr2 ((ac, bc), InUserMode) PSched ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) (part ((a, b), InUserMode)) ((a, b), InUserMode); uwr2 ((ac, bc), InUserMode) u ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); policy2 (part ((a, b), InUserMode)) u; part ((a, b), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((ac, bc), InUserMode) = part ((a, b), InUserMode); invs_if ((ac, bc), InUserMode); invs_if ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ad, bd), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); invs_if ((ad, bd), KernelEntry Interrupt); invs_if ((ab, bb), InUserMode); step_restrict ((ad, bd), KernelEntry Interrupt); step_restrict ((ab, bb), InUserMode); t = ((a, b), InUserMode); t' = ((ab, bb), InUserMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf; s = ((ac, bc), InUserMode); s' = ((ad, bd), KernelEntry Interrupt); ((ac, bc), Some i, ad, bd) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((ad, bd), KernelEntry Interrupt) u ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) PSched ((ab, bb), InUserMode) \<and> uwr2 ((ad, bd), KernelEntry Interrupt) (part ((a, b), InUserMode)) ((ab, bb), InUserMode)
 2. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 7. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InUserMode) PSched ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) (part ((ab, bb), InUserMode)) ((ab, bb), InUserMode); uwr2 ((a, b), InUserMode) u ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((a, b), InUserMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InUserMode); policy2 (part ((ab, bb), InUserMode)) u; part ((ab, bb), InUserMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InUserMode) = part ((ab, bb), InUserMode); invs_if ((a, b), InUserMode); invs_if ((ab, bb), InUserMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InUserMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InUserMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InUserMode)) ((ac, bc), KernelEntry Interrupt)
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; InIdleMode = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; InIdleMode = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = InIdleMode\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (8 subgoals):
 1. \<And>a b aa ba i ab bb ac bc ia. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InIdleMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some ia, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InIdleMode)) ((ac, bc), KernelEntry Interrupt)
 2. \<And>a b aa ba i ab bb ac bc. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), InIdleMode); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), InIdleMode); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), InIdleMode); s = ((a, b), InIdleMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), InIdleMode); ((ab, bb), None, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InIdleMode)) ((ac, bc), InIdleMode)
 3. \<And>a b aa ba ab bb ac bc i. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), InIdleMode); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), InIdleMode); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InIdleMode); s' = ((aa, ba), InIdleMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some i, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), InIdleMode) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), InIdleMode) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), InIdleMode) (part ((ab, bb), InIdleMode)) ((ac, bc), KernelEntry Interrupt)
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InIdleMode); invs_if ((aa, ba), InIdleMode); invs_if ((ac, bc), InIdleMode); step_restrict ((aa, ba), InIdleMode); step_restrict ((ac, bc), InIdleMode); s = ((a, b), InIdleMode); s' = ((aa, ba), InIdleMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), InIdleMode); ((ab, bb), None, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), InIdleMode) u ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), InIdleMode) PSched ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), InIdleMode) (part ((ab, bb), InIdleMode)) ((ac, bc), InIdleMode)
 5. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 7. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 8. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba i ab bb ac bc. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelEntry Interrupt); system.reachable (ADT_A_if utf) s0 ((ac, bc), InIdleMode); invs_if ((aa, ba), KernelEntry Interrupt); invs_if ((ac, bc), InIdleMode); step_restrict ((aa, ba), KernelEntry Interrupt); step_restrict ((ac, bc), InIdleMode); s = ((a, b), InIdleMode); s' = ((aa, ba), KernelEntry Interrupt); ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), InIdleMode); ((ab, bb), None, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelEntry Interrupt) u ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) PSched ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), KernelEntry Interrupt) (part ((ab, bb), InIdleMode)) ((ac, bc), InIdleMode)
 2. \<And>a b aa ba ab bb ac bc i. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), InIdleMode); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), InIdleMode); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InIdleMode); s' = ((aa, ba), InIdleMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some i, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), InIdleMode) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), InIdleMode) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), InIdleMode) (part ((ab, bb), InIdleMode)) ((ac, bc), KernelEntry Interrupt)
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InIdleMode); invs_if ((aa, ba), InIdleMode); invs_if ((ac, bc), InIdleMode); step_restrict ((aa, ba), InIdleMode); step_restrict ((ac, bc), InIdleMode); s = ((a, b), InIdleMode); s' = ((aa, ba), InIdleMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), InIdleMode); ((ab, bb), None, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), InIdleMode) u ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), InIdleMode) PSched ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), InIdleMode) (part ((ab, bb), InIdleMode)) ((ac, bc), InIdleMode)
 4. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 7. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba ab bb ac bc i. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelEntry Interrupt); invs_if ((aa, ba), InIdleMode); invs_if ((ac, bc), KernelEntry Interrupt); step_restrict ((aa, ba), InIdleMode); step_restrict ((ac, bc), KernelEntry Interrupt); s = ((a, b), InIdleMode); s' = ((aa, ba), InIdleMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), KernelEntry Interrupt); ((ab, bb), Some i, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), InIdleMode) u ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), InIdleMode) PSched ((ac, bc), KernelEntry Interrupt) \<and> uwr2 ((aa, ba), InIdleMode) (part ((ab, bb), InIdleMode)) ((ac, bc), KernelEntry Interrupt)
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InIdleMode); invs_if ((aa, ba), InIdleMode); invs_if ((ac, bc), InIdleMode); step_restrict ((aa, ba), InIdleMode); step_restrict ((ac, bc), InIdleMode); s = ((a, b), InIdleMode); s' = ((aa, ba), InIdleMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), InIdleMode); ((ab, bb), None, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), InIdleMode) u ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), InIdleMode) PSched ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), InIdleMode) (part ((ab, bb), InIdleMode)) ((ac, bc), InIdleMode)
 3. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>uwr2 ((a, b), InIdleMode) PSched ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) (part ((ab, bb), InIdleMode)) ((ab, bb), InIdleMode); uwr2 ((a, b), InIdleMode) u ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((a, b), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ab, bb), InIdleMode); policy2 (part ((ab, bb), InIdleMode)) u; part ((ab, bb), InIdleMode) \<noteq> PSched; u \<noteq> PSched; part ((a, b), InIdleMode) = part ((ab, bb), InIdleMode); invs_if ((a, b), InIdleMode); invs_if ((ab, bb), InIdleMode); system.reachable (ADT_A_if utf) s0 ((aa, ba), InIdleMode); system.reachable (ADT_A_if utf) s0 ((ac, bc), InIdleMode); invs_if ((aa, ba), InIdleMode); invs_if ((ac, bc), InIdleMode); step_restrict ((aa, ba), InIdleMode); step_restrict ((ac, bc), InIdleMode); s = ((a, b), InIdleMode); s' = ((aa, ba), InIdleMode); ((a, b), None, aa, ba) \<in> check_active_irq_A_if; t = ((ab, bb), InIdleMode); t' = ((ac, bc), InIdleMode); ((ab, bb), None, ac, bc) \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), InIdleMode) u ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), InIdleMode) PSched ((ac, bc), InIdleMode) \<and> uwr2 ((aa, ba), InIdleMode) (part ((ab, bb), InIdleMode)) ((ac, bc), InIdleMode)
 2. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelEntry x3\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (4 subgoals):
 1. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry x3 = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (4 subgoals):
 1. \<And>x3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry x3 = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (4 subgoals):
 1. \<And>event. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry event = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (5 subgoals):
 1. \<And>event. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry event = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t; event \<noteq> Interrupt\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<And>event. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry event = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t\<rbrakk> \<Longrightarrow> event \<noteq> Interrupt
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (5 subgoals):
 1. \<And>event. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry event = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t\<rbrakk> \<Longrightarrow> event \<noteq> Interrupt
 2. \<And>event. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry event = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t; event \<noteq> Interrupt\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (5 subgoals):
 1. \<And>event a b. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); ((a, b), t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched (a, b); uwr2 s (part (a, b)) (a, b); uwr2 s u (a, b); system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 (a, b); policy2 (part (a, b)) u; part (a, b) \<noteq> PSched; u \<noteq> PSched; part s = part (a, b); KernelEntry event = sys_mode_of (a, b); invs_if s; invs_if (a, b); system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of (a, b); t = (a, b)\<rbrakk> \<Longrightarrow> event \<noteq> Interrupt
 2. \<And>event. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry event = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t; event \<noteq> Interrupt\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (4 subgoals):
 1. \<And>event. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelEntry event = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = sys_mode_of t; event \<noteq> Interrupt\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (7 subgoals):
 1. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((a, b), KernelEntry ea) PSched ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) (part ((ab, bb), KernelEntry ea)) ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) u ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry ea); policy2 (part ((ab, bb), KernelEntry ea)) u; part ((ab, bb), KernelEntry ea) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelEntry ea) = part ((ab, bb), KernelEntry ea); event = ea; invs_if ((a, b), KernelEntry ea); invs_if ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelPreempted); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelPreempted); invs_if ((aa, ba), KernelPreempted); invs_if ((ac, bc), KernelPreempted); e = ea; step_restrict ((aa, ba), KernelPreempted); step_restrict ((ac, bc), KernelPreempted); s = ((a, b), KernelEntry ea); s' = ((aa, ba), KernelPreempted); ((a, b), True, aa, ba) \<in> kernel_call_A_if ea; t = ((ab, bb), KernelEntry ea); t' = ((ac, bc), KernelPreempted); ((ab, bb), True, ac, bc) \<in> kernel_call_A_if ea; ea \<noteq> Interrupt\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelPreempted) u ((ac, bc), KernelPreempted) \<and> uwr2 ((aa, ba), KernelPreempted) PSched ((ac, bc), KernelPreempted) \<and> uwr2 ((aa, ba), KernelPreempted) (part ((ab, bb), KernelEntry ea)) ((ac, bc), KernelPreempted)
 2. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((a, b), KernelEntry ea) PSched ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) (part ((ab, bb), KernelEntry ea)) ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) u ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry ea); policy2 (part ((ab, bb), KernelEntry ea)) u; part ((ab, bb), KernelEntry ea) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelEntry ea) = part ((ab, bb), KernelEntry ea); event = ea; invs_if ((a, b), KernelEntry ea); invs_if ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelPreempted); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelPreempted); invs_if ((ac, bc), KernelSchedule False); e = ea; ea \<noteq> Interrupt; step_restrict ((aa, ba), KernelPreempted); step_restrict ((ac, bc), KernelSchedule False); s = ((a, b), KernelEntry ea); s' = ((aa, ba), KernelPreempted); ((a, b), True, aa, ba) \<in> kernel_call_A_if ea; t = ((ab, bb), KernelEntry ea); t' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if ea\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelPreempted) u ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelPreempted) PSched ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelPreempted) (part ((ab, bb), KernelEntry ea)) ((ac, bc), KernelSchedule False)
 3. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((ab, bb), KernelEntry e) PSched ((a, b), KernelEntry e); uwr2 ((ab, bb), KernelEntry e) (part ((a, b), KernelEntry e)) ((a, b), KernelEntry e); uwr2 ((ab, bb), KernelEntry e) u ((a, b), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry e); policy2 (part ((a, b), KernelEntry e)) u; part ((a, b), KernelEntry e) \<noteq> PSched; u \<noteq> PSched; part ((ab, bb), KernelEntry e) = part ((a, b), KernelEntry e); event = e; invs_if ((ab, bb), KernelEntry e); invs_if ((a, b), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelPreempted); invs_if ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelPreempted); ea = e; step_restrict ((ac, bc), KernelSchedule False); step_restrict ((aa, ba), KernelPreempted); t = ((a, b), KernelEntry e); t' = ((aa, ba), KernelPreempted); ((a, b), True, aa, ba) \<in> kernel_call_A_if e; e \<noteq> Interrupt; s = ((ab, bb), KernelEntry e); s' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if e\<rbrakk> \<Longrightarrow> uwr2 ((ac, bc), KernelSchedule False) u ((aa, ba), KernelPreempted) \<and> uwr2 ((ac, bc), KernelSchedule False) PSched ((aa, ba), KernelPreempted) \<and> uwr2 ((ac, bc), KernelSchedule False) (part ((a, b), KernelEntry e)) ((aa, ba), KernelPreempted)
 4. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((a, b), KernelEntry ea) PSched ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) (part ((ab, bb), KernelEntry ea)) ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) u ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry ea); policy2 (part ((ab, bb), KernelEntry ea)) u; part ((ab, bb), KernelEntry ea) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelEntry ea) = part ((ab, bb), KernelEntry ea); event = ea; invs_if ((a, b), KernelEntry ea); invs_if ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelSchedule False); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelSchedule False); invs_if ((ac, bc), KernelSchedule False); e = ea; ea \<noteq> Interrupt; step_restrict ((aa, ba), KernelSchedule False); step_restrict ((ac, bc), KernelSchedule False); s = ((a, b), KernelEntry ea); s' = ((aa, ba), KernelSchedule False); ((a, b), False, aa, ba) \<in> kernel_call_A_if ea; t = ((ab, bb), KernelEntry ea); t' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if ea\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelSchedule False) u ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelSchedule False) PSched ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelSchedule False) (part ((ab, bb), KernelEntry ea)) ((ac, bc), KernelSchedule False)
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 7. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (6 subgoals):
 1. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((a, b), KernelEntry ea) PSched ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) (part ((ab, bb), KernelEntry ea)) ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) u ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry ea); policy2 (part ((ab, bb), KernelEntry ea)) u; part ((ab, bb), KernelEntry ea) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelEntry ea) = part ((ab, bb), KernelEntry ea); event = ea; invs_if ((a, b), KernelEntry ea); invs_if ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelPreempted); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelPreempted); invs_if ((ac, bc), KernelSchedule False); e = ea; ea \<noteq> Interrupt; step_restrict ((aa, ba), KernelPreempted); step_restrict ((ac, bc), KernelSchedule False); s = ((a, b), KernelEntry ea); s' = ((aa, ba), KernelPreempted); ((a, b), True, aa, ba) \<in> kernel_call_A_if ea; t = ((ab, bb), KernelEntry ea); t' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if ea\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelPreempted) u ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelPreempted) PSched ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelPreempted) (part ((ab, bb), KernelEntry ea)) ((ac, bc), KernelSchedule False)
 2. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((ab, bb), KernelEntry e) PSched ((a, b), KernelEntry e); uwr2 ((ab, bb), KernelEntry e) (part ((a, b), KernelEntry e)) ((a, b), KernelEntry e); uwr2 ((ab, bb), KernelEntry e) u ((a, b), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry e); policy2 (part ((a, b), KernelEntry e)) u; part ((a, b), KernelEntry e) \<noteq> PSched; u \<noteq> PSched; part ((ab, bb), KernelEntry e) = part ((a, b), KernelEntry e); event = e; invs_if ((ab, bb), KernelEntry e); invs_if ((a, b), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelPreempted); invs_if ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelPreempted); ea = e; step_restrict ((ac, bc), KernelSchedule False); step_restrict ((aa, ba), KernelPreempted); t = ((a, b), KernelEntry e); t' = ((aa, ba), KernelPreempted); ((a, b), True, aa, ba) \<in> kernel_call_A_if e; e \<noteq> Interrupt; s = ((ab, bb), KernelEntry e); s' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if e\<rbrakk> \<Longrightarrow> uwr2 ((ac, bc), KernelSchedule False) u ((aa, ba), KernelPreempted) \<and> uwr2 ((ac, bc), KernelSchedule False) PSched ((aa, ba), KernelPreempted) \<and> uwr2 ((ac, bc), KernelSchedule False) (part ((a, b), KernelEntry e)) ((aa, ba), KernelPreempted)
 3. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((a, b), KernelEntry ea) PSched ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) (part ((ab, bb), KernelEntry ea)) ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) u ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry ea); policy2 (part ((ab, bb), KernelEntry ea)) u; part ((ab, bb), KernelEntry ea) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelEntry ea) = part ((ab, bb), KernelEntry ea); event = ea; invs_if ((a, b), KernelEntry ea); invs_if ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelSchedule False); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelSchedule False); invs_if ((ac, bc), KernelSchedule False); e = ea; ea \<noteq> Interrupt; step_restrict ((aa, ba), KernelSchedule False); step_restrict ((ac, bc), KernelSchedule False); s = ((a, b), KernelEntry ea); s' = ((aa, ba), KernelSchedule False); ((a, b), False, aa, ba) \<in> kernel_call_A_if ea; t = ((ab, bb), KernelEntry ea); t' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if ea\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelSchedule False) u ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelSchedule False) PSched ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelSchedule False) (part ((ab, bb), KernelEntry ea)) ((ac, bc), KernelSchedule False)
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 6. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (5 subgoals):
 1. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((ab, bb), KernelEntry e) PSched ((a, b), KernelEntry e); uwr2 ((ab, bb), KernelEntry e) (part ((a, b), KernelEntry e)) ((a, b), KernelEntry e); uwr2 ((ab, bb), KernelEntry e) u ((a, b), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry e); policy2 (part ((a, b), KernelEntry e)) u; part ((a, b), KernelEntry e) \<noteq> PSched; u \<noteq> PSched; part ((ab, bb), KernelEntry e) = part ((a, b), KernelEntry e); event = e; invs_if ((ab, bb), KernelEntry e); invs_if ((a, b), KernelEntry e); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelPreempted); invs_if ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelPreempted); ea = e; step_restrict ((ac, bc), KernelSchedule False); step_restrict ((aa, ba), KernelPreempted); t = ((a, b), KernelEntry e); t' = ((aa, ba), KernelPreempted); ((a, b), True, aa, ba) \<in> kernel_call_A_if e; e \<noteq> Interrupt; s = ((ab, bb), KernelEntry e); s' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if e\<rbrakk> \<Longrightarrow> uwr2 ((ac, bc), KernelSchedule False) u ((aa, ba), KernelPreempted) \<and> uwr2 ((ac, bc), KernelSchedule False) PSched ((aa, ba), KernelPreempted) \<and> uwr2 ((ac, bc), KernelSchedule False) (part ((a, b), KernelEntry e)) ((aa, ba), KernelPreempted)
 2. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((a, b), KernelEntry ea) PSched ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) (part ((ab, bb), KernelEntry ea)) ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) u ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry ea); policy2 (part ((ab, bb), KernelEntry ea)) u; part ((ab, bb), KernelEntry ea) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelEntry ea) = part ((ab, bb), KernelEntry ea); event = ea; invs_if ((a, b), KernelEntry ea); invs_if ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelSchedule False); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelSchedule False); invs_if ((ac, bc), KernelSchedule False); e = ea; ea \<noteq> Interrupt; step_restrict ((aa, ba), KernelSchedule False); step_restrict ((ac, bc), KernelSchedule False); s = ((a, b), KernelEntry ea); s' = ((aa, ba), KernelSchedule False); ((a, b), False, aa, ba) \<in> kernel_call_A_if ea; t = ((ab, bb), KernelEntry ea); t' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if ea\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelSchedule False) u ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelSchedule False) PSched ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelSchedule False) (part ((ab, bb), KernelEntry ea)) ((ac, bc), KernelSchedule False)
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (4 subgoals):
 1. \<And>event a b aa ba e ab bb ac bc ea. \<lbrakk>uwr2 ((a, b), KernelEntry ea) PSched ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) (part ((ab, bb), KernelEntry ea)) ((ab, bb), KernelEntry ea); uwr2 ((a, b), KernelEntry ea) u ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((a, b), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelEntry ea); policy2 (part ((ab, bb), KernelEntry ea)) u; part ((ab, bb), KernelEntry ea) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelEntry ea) = part ((ab, bb), KernelEntry ea); event = ea; invs_if ((a, b), KernelEntry ea); invs_if ((ab, bb), KernelEntry ea); system.reachable (ADT_A_if utf) s0 ((aa, ba), KernelSchedule False); system.reachable (ADT_A_if utf) s0 ((ac, bc), KernelSchedule False); invs_if ((aa, ba), KernelSchedule False); invs_if ((ac, bc), KernelSchedule False); e = ea; ea \<noteq> Interrupt; step_restrict ((aa, ba), KernelSchedule False); step_restrict ((ac, bc), KernelSchedule False); s = ((a, b), KernelEntry ea); s' = ((aa, ba), KernelSchedule False); ((a, b), False, aa, ba) \<in> kernel_call_A_if ea; t = ((ab, bb), KernelEntry ea); t' = ((ac, bc), KernelSchedule False); ((ab, bb), False, ac, bc) \<in> kernel_call_A_if ea\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), KernelSchedule False) u ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelSchedule False) PSched ((ac, bc), KernelSchedule False) \<and> uwr2 ((aa, ba), KernelSchedule False) (part ((ab, bb), KernelEntry ea)) ((ac, bc), KernelSchedule False)
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 4. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelPreempted = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelPreempted = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelPreempted\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 3. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (2 subgoals):
 1. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (2 subgoals):
 1. \<And>x5. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelSchedule x5\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t'
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (2 subgoals):
 1. \<And>x5 a b ba aa bb ab bc bd ac be. \<lbrakk>uwr2 ((a, b), KernelSchedule bd) PSched ((ab, bc), KernelSchedule bd); uwr2 ((a, b), KernelSchedule bd) (part ((ab, bc), KernelSchedule bd)) ((ab, bc), KernelSchedule bd); uwr2 ((a, b), KernelSchedule bd) u ((ab, bc), KernelSchedule bd); system.reachable (ADT_A_if utf) s0 ((a, b), KernelSchedule bd); system.reachable (ADT_A_if utf) s0 ((ab, bc), KernelSchedule bd); policy2 (part ((ab, bc), KernelSchedule bd)) u; part ((ab, bc), KernelSchedule bd) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelSchedule bd) = part ((ab, bc), KernelSchedule bd); x5 = bd; invs_if ((a, b), KernelSchedule bd); invs_if ((ab, bc), KernelSchedule bd); system.reachable (ADT_A_if utf) s0 ((aa, bb), KernelExit); system.reachable (ADT_A_if utf) s0 ((ac, be), KernelExit); invs_if ((aa, bb), KernelExit); invs_if ((ac, be), KernelExit); ba = bd; step_restrict ((aa, bb), KernelExit); step_restrict ((ac, be), KernelExit); s = ((a, b), KernelSchedule bd); s' = ((aa, bb), KernelExit); ((a, b), (), aa, bb) \<in> kernel_schedule_if; t = ((ab, bc), KernelSchedule bd); t' = ((ac, be), KernelExit); ((ab, bc), (), ac, be) \<in> kernel_schedule_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, bb), KernelExit) u ((ac, be), KernelExit) \<and> uwr2 ((aa, bb), KernelExit) PSched ((ac, be), KernelExit) \<and> uwr2 ((aa, bb), KernelExit) (part ((ab, bc), KernelSchedule bd)) ((ac, be), KernelExit)
 2. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; sys_mode_of s = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelExit = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); uwr2 s PSched t; uwr2 s (part t) t; uwr2 s u t; system.reachable (ADT_A_if utf) s0 s; system.reachable (ADT_A_if utf) s0 t; policy2 (part t) u; part t \<noteq> PSched; u \<noteq> PSched; part s = part t; KernelExit = sys_mode_of t; invs_if s; invs_if t; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 t'; invs_if s'; invs_if t'; sys_mode_of s = KernelExit\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part t) t' proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba m ab bb ac bc ma. \<lbrakk>uwr2 ((a, b), KernelExit) PSched ((ab, bb), KernelExit); uwr2 ((a, b), KernelExit) (part ((ab, bb), KernelExit)) ((ab, bb), KernelExit); uwr2 ((a, b), KernelExit) u ((ab, bb), KernelExit); system.reachable (ADT_A_if utf) s0 ((a, b), KernelExit); system.reachable (ADT_A_if utf) s0 ((ab, bb), KernelExit); policy2 (part ((ab, bb), KernelExit)) u; part ((ab, bb), KernelExit) \<noteq> PSched; u \<noteq> PSched; part ((a, b), KernelExit) = part ((ab, bb), KernelExit); invs_if ((a, b), KernelExit); invs_if ((ab, bb), KernelExit); system.reachable (ADT_A_if utf) s0 ((aa, ba), m); system.reachable (ADT_A_if utf) s0 ((ac, bc), ma); invs_if ((aa, ba), m); invs_if ((ac, bc), ma); step_restrict ((aa, ba), m); step_restrict ((ac, bc), ma); s = ((a, b), KernelExit); s' = ((aa, ba), m); ((a, b), m, aa, ba) \<in> kernel_exit_A_if; t = ((ab, bb), KernelExit); t' = ((ac, bc), ma); ((ab, bb), ma, ac, bc) \<in> kernel_exit_A_if\<rbrakk> \<Longrightarrow> uwr2 ((aa, ba), m) u ((ac, bc), ma) \<and> uwr2 ((aa, ba), m) PSched ((ac, bc), ma) \<and> uwr2 ((aa, ba), m) (part ((ab, bb), KernelExit)) ((ac, bc), ma) proof (prove)
goal:
No subgoals!