theory ADT_IF_Refine

lemma conc_serial:
  assumes uop_sane: "\<And>s e t. (s,e,t) \<in> do_user_op_conc \<Longrightarrow>
                       e \<noteq> Some Interrupt"
  assumes no_fail: "nf"
  shows
    "serial_system (ADT_conc) {s'. \<exists>s. (s,s') \<in> (lift_fst_rel srel) \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}" apply (insert no_fail) apply (unfold_locales) apply (rule fw_inv_transport) apply (rule abs.ADT_invs) apply (rule conc.ADT_invs) apply (rule fw_sim_abs_conc) apply (clarsimp simp: conc.step_adt global_automaton_if_def lift_fst_rel_def) apply (case_tac ba,simp_all) apply (rule step_corres_exE[OF corres_check_active_irq],assumption+) apply (rule preservesE[OF conc.check_active_irq_invs],assumption+) apply (rule preservesE[OF abs.check_active_irq_invs],assumption+) apply (rule_tac s=t and s'=t' in step_corres_exE[OF corres_do_user_op],assumption+) apply (rule_tac s=t and s'=t' in step_corresE[OF corres_do_user_op],assumption+) apply clarsimp apply (case_tac e) apply (case_tac ea) apply fastforce apply simp apply (frule uop_sane) apply fastforce apply (case_tac ea) apply fastforce apply fastforce apply (rule step_corres_exE[OF corres_check_active_irq_idle],assumption+) apply (case_tac e) apply fastforce apply fastforce apply clarsimp apply (rule step_corres_exE[OF corres_kernel_call],assumption+) apply (case_tac e ; fastforce dest: kernel_call_no_preempt) apply (rule step_corres_exE[OF corres_handle_preemption],assumption+) apply fastforce apply (rule step_corres_exE[OF corres_schedule],assumption+) apply fastforce apply (rule step_corres_exE[OF corres_kernel_exit],assumption+) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. serial_system ADT_conc {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} proof (prove)
goal (1 subgoal):
 1. nf \<Longrightarrow> serial_system ADT_conc {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} proof (prove)
goal (2 subgoals):
 1. nf \<Longrightarrow> ADT_conc \<Turnstile> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}
 2. \<And>s' a. \<lbrakk>nf; s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step ADT_conc a proof (prove)
goal (4 subgoals):
 1. nf \<Longrightarrow> ?A2 \<Turnstile> invs_abs
 2. nf \<Longrightarrow> ADT_conc \<Turnstile> invs_conc
 3. nf \<Longrightarrow> LI ?A2 ADT_conc (lift_fst_rel srel) (invs_abs \<times> invs_conc)
 4. \<And>s' a. \<lbrakk>nf; s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step ADT_conc a proof (prove)
goal (3 subgoals):
 1. nf \<Longrightarrow> ADT_conc \<Turnstile> invs_conc
 2. nf \<Longrightarrow> LI ADT_abs ADT_conc (lift_fst_rel srel) (invs_abs \<times> invs_conc)
 3. \<And>s' a. \<lbrakk>nf; s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step ADT_conc a proof (prove)
goal (2 subgoals):
 1. nf \<Longrightarrow> LI ADT_abs ADT_conc (lift_fst_rel srel) (invs_abs \<times> invs_conc)
 2. \<And>s' a. \<lbrakk>nf; s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step ADT_conc a proof (prove)
goal (1 subgoal):
 1. \<And>s' a. \<lbrakk>nf; s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step ADT_conc a proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), ba) \<in> invs_abs; ((a, b), ba) \<in> invs_conc\<rbrakk> \<Longrightarrow> \<exists>aa bb bc. (\<exists>e. ba = KernelEntry e \<and> bc = KernelPreempted \<and> ((a, b), True, aa, bb) \<in> kernel_call_conc e \<and> e \<noteq> Interrupt) \<or> (\<exists>e. ba = KernelEntry e \<and> bc = KernelSchedule (e = Interrupt) \<and> ((a, b), False, aa, bb) \<in> kernel_call_conc e) \<or> ba = KernelPreempted \<and> bc = KernelSchedule True \<and> ((a, b), (), aa, bb) \<in> handle_preemption_conc \<or> (\<exists>b. ba = KernelSchedule b) \<and> bc = KernelExit \<and> ((a, b), (), aa, bb) \<in> schedule_conc \<or> ba = KernelExit \<and> ((a, b), bc, aa, bb) \<in> kernel_exit_conc \<or> ba = InUserMode \<and> (\<exists>ab ba e. bc = KernelEntry e \<and> ((a, b), None, ab, ba) \<in> check_active_irq_conc \<and> ((ab, ba), Some e, aa, bb) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> ba = InUserMode \<and> bc = InUserMode \<and> (\<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_conc \<and> ((ab, ba), None, aa, bb) \<in> do_user_op_conc) \<or> ba = InUserMode \<and> bc = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, bb) \<in> check_active_irq_conc) \<or> ba = InIdleMode \<and> bc = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, bb) \<in> check_active_irq_conc) \<or> ba = InIdleMode \<and> bc = InIdleMode \<and> ((a, b), None, aa, bb) \<in> check_active_irq_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ba = InUserMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ba = InUserMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ba = InUserMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel; (t', InUserMode) \<in> invs_conc\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ba = InUserMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel; (t', InUserMode) \<in> invs_conc; (t, InUserMode) \<in> invs_abs\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb e t' t ea t'a ta. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ba = InUserMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel; (t', InUserMode) \<in> invs_conc; (t, InUserMode) \<in> invs_abs; (t', ea, t'a) \<in> do_user_op_conc; (t, ea, ta) \<in> do_user_op_abs; (ta, t'a) \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb e t' t ea t'a ta tb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ba = InUserMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel; (t', InUserMode) \<in> invs_conc; (t, InUserMode) \<in> invs_abs; (t', ea, t'a) \<in> do_user_op_conc; (t, ea, ta) \<in> do_user_op_abs; (ta, t'a) \<in> srel; (t, ea, tb) \<in> do_user_op_abs; (tb, t'a) \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (7 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = None\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 4. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 5. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 6. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 7. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (8 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = None; ea = None\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = None; ea = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 3. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 5. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 7. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 8. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (7 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = None; ea = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 4. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 5. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 6. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 7. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (7 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), None, ab, bc) \<in> check_active_irq_conc; ((aa, bb), None, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), Some ag, ad, be) \<in> do_user_op_conc; ((ac, bd), Some ag, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), Some ag, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = None; ea = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 4. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 5. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 6. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 7. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (7 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), None, ab, bc) \<in> check_active_irq_conc; ((aa, bb), None, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), Some ag, ad, be) \<in> do_user_op_conc; ((ac, bd), Some ag, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), Some ag, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = None; ea = Some ag; Some ag \<noteq> Some Interrupt\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 4. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 5. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 6. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 7. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (7 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag; ea = None\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag ah. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag; ea = Some ah\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 4. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 5. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 6. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 7. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b aa bb e ab bc ac bd ea ad be ae bf af bg ag ah. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InUserMode) \<in> invs_abs; ((a, b), InUserMode) \<in> invs_conc; ((a, b), e, ab, bc) \<in> check_active_irq_conc; ((aa, bb), e, ac, bd) \<in> check_active_irq_abs; ((ac, bd), ab, bc) \<in> srel; ((ab, bc), InUserMode) \<in> invs_conc; ((ac, bd), InUserMode) \<in> invs_abs; ((ab, bc), ea, ad, be) \<in> do_user_op_conc; ((ac, bd), ea, ae, bf) \<in> do_user_op_abs; ((ae, bf), ad, be) \<in> srel; ((ac, bd), ea, af, bg) \<in> do_user_op_abs; ((af, bg), ad, be) \<in> srel; e = Some ag; ea = Some ah\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. (\<exists>ab bc e. bb = KernelEntry e \<and> ((a, b), None, ab, bc) \<in> check_active_irq_conc \<and> ((ab, bc), Some e, aa, ba) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> bb = InUserMode \<and> (\<exists>ab bb. ((a, b), None, ab, bb) \<in> check_active_irq_conc \<and> ((ab, bb), None, aa, ba) \<in> do_user_op_conc) \<or> bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc)
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (5 subgoals):
 1. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 2. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 4. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 5. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (5 subgoals):
 1. \<And>a b ba aa bb e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 2. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 4. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 5. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel; e = None\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 2. \<And>a b ba aa bb e t' t ab. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel; e = Some ab\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 3. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 5. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 6. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (5 subgoals):
 1. \<And>a b ba aa bb e t' t ab. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), InIdleMode) \<in> invs_abs; ((a, b), InIdleMode) \<in> invs_conc; ba = InIdleMode; ((a, b), e, t') \<in> check_active_irq_conc; ((aa, bb), e, t) \<in> check_active_irq_abs; (t, t') \<in> srel; e = Some ab\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_conc) \<or> bb = InIdleMode \<and> ((a, b), None, aa, ba) \<in> check_active_irq_conc
 2. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 4. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 5. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (4 subgoals):
 1. \<And>a b ba aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ba = KernelEntry x3\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 3. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (4 subgoals):
 1. \<And>a b aa bb x3. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 3. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (4 subgoals):
 1. \<And>a b aa bb x3 e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelEntry x3) \<in> invs_abs; ((a, b), KernelEntry x3) \<in> invs_conc; ((a, b), e, t') \<in> kernel_call_conc x3; ((aa, bb), e, t) \<in> kernel_call_abs x3; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. bb = KernelPreempted \<and> ((a, b), True, aa, ba) \<in> kernel_call_conc x3 \<and> x3 \<noteq> Interrupt \<or> bb = KernelSchedule (x3 = Interrupt) \<and> ((a, b), False, aa, ba) \<in> kernel_call_conc x3
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 3. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 4. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (3 subgoals):
 1. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 2. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (3 subgoals):
 1. \<And>a b ba aa bb e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelPreempted) \<in> invs_abs; ((a, b), KernelPreempted) \<in> invs_conc; ba = KernelPreempted; ((a, b), e, t') \<in> handle_preemption_conc; ((aa, bb), e, t) \<in> handle_preemption_abs; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> handle_preemption_conc
 2. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 3. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb x5. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb x5 e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelSchedule x5) \<in> invs_abs; ((a, b), KernelSchedule x5) \<in> invs_conc; ba = KernelSchedule x5; ((a, b), e, t') \<in> schedule_conc; ((aa, bb), e, t) \<in> schedule_abs; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((a, b), (), aa, ba) \<in> schedule_conc
 2. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb e t' t. \<lbrakk>nf; ((aa, bb), a, b) \<in> srel; ((aa, bb), KernelExit) \<in> invs_abs; ((a, b), KernelExit) \<in> invs_conc; ba = KernelExit; ((a, b), e, t') \<in> kernel_exit_conc; ((aa, bb), e, t) \<in> kernel_exit_abs; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa ba bb. ((a, b), bb, aa, ba) \<in> kernel_exit_conc proof (prove)
goal:
No subgoals!