theory ADT_IF_Refine

lemma fw_sim_abs_conc:
  "LI (ADT_abs) (ADT_conc) (lift_fst_rel srel) (invs_abs \<times> invs_conc)" apply (unfold LI_def ) apply (intro conjI allI) apply (rule init_refinement) apply (clarsimp simp: rel_semi_def relcomp_unfold lift_fst_rel_def
                         abs.step_adt conc.step_adt) apply (clarsimp simp: global_automaton_if_def) apply (elim disjE exE conjE,simp_all) apply (rule step_corres_bothE[OF corres_kernel_call conc.kernel_call_invs],assumption+,auto)[1] apply (rule step_corres_bothE[OF corres_kernel_call conc.kernel_call_invs_sched],assumption+,auto)[1] apply (rule step_corres_bothE[OF corres_handle_preemption conc.handle_preemption_invs],assumption+,auto)[1] apply (rule step_corres_bothE[OF corres_schedule conc.schedule_invs],assumption+,auto)[1] apply (rule step_corres_both'E[OF corres_kernel_exit conc.kernel_exit_invs],assumption+,auto)[1] apply (rule preservesE[OF conc.check_active_irq_invs],assumption+) apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs],assumption+,clarsimp) apply (rule preservesE[OF abs.check_active_irq_invs],assumption+) apply (rule_tac s'="(ac,be)" in step_corres_bothE[OF corres_do_user_op conc.do_user_op_invs_entry],assumption+,auto)[1] apply (rule preservesE[OF conc.check_active_irq_invs],assumption+) apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs],assumption+,clarsimp) apply (rule preservesE[OF abs.check_active_irq_invs],assumption+) apply (rule_tac s'="(ac,be)" in step_corres_bothE[OF corres_do_user_op conc.do_user_op_invs],assumption+,auto)[1] apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs_entry],assumption+,auto)[1] apply (rule step_corres_bothE[OF corres_check_active_irq_idle conc.check_active_irq_idle_invs_entry],assumption+,auto)[1] apply (rule preservesE[OF conc.check_active_irq_idle_invs],assumption+) apply (rule step_corres_bothE[OF corres_check_active_irq_idle conc.check_active_irq_idle_invs],assumption+,auto)[1] apply (fastforce intro!: srel_Fin simp: lift_fst_rel_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LI ADT_abs ADT_conc (lift_fst_rel srel) (invs_abs \<times> invs_conc) proof (prove)
goal (1 subgoal):
 1. (\<forall>s. Init ADT_conc s \<subseteq> lift_fst_rel srel `` Init ADT_abs s) \<and> (\<forall>j. lift_fst_rel srel \<inter> invs_abs \<times> invs_conc ;;; Step ADT_conc j \<subseteq> Step ADT_abs j ;;; lift_fst_rel srel) \<and> (\<forall>s s'. (s, s') \<in> lift_fst_rel srel \<inter> invs_abs \<times> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s) proof (prove)
goal (3 subgoals):
 1. \<And>s. Init ADT_conc s \<subseteq> lift_fst_rel srel `` Init ADT_abs s
 2. \<And>j. lift_fst_rel srel \<inter> invs_abs \<times> invs_conc ;;; Step ADT_conc j \<subseteq> Step ADT_abs j ;;; lift_fst_rel srel
 3. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<inter> invs_abs \<times> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (2 subgoals):
 1. \<And>j. lift_fst_rel srel \<inter> invs_abs \<times> invs_conc ;;; Step ADT_conc j \<subseteq> Step ADT_abs j ;;; lift_fst_rel srel
 2. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<inter> invs_abs \<times> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), ba) \<in> invs_abs; ((ab, bd), ba) \<in> invs_conc; (((ab, bd), ba), (aa, bb), bc) \<in> global_automaton_if check_active_irq_conc do_user_op_conc kernel_call_conc handle_preemption_conc schedule_conc kernel_exit_conc\<rbrakk> \<Longrightarrow> \<exists>ab bd. (((a, b), ba), (ab, bd), bc) \<in> global_automaton_if check_active_irq_abs do_user_op_abs kernel_call_abs handle_preemption_abs schedule_abs kernel_exit_abs \<and> ((ab, bd), bc) \<in> extras_abs \<and> ((ab, bd), aa, bb) \<in> srel
 2. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<inter> invs_abs \<times> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), ba) \<in> invs_abs; ((ab, bd), ba) \<in> invs_conc; (\<exists>e. ba = KernelEntry e \<and> bc = KernelPreempted \<and> ((ab, bd), True, aa, bb) \<in> kernel_call_conc e \<and> e \<noteq> Interrupt) \<or> (\<exists>e. ba = KernelEntry e \<and> bc = KernelSchedule (e = Interrupt) \<and> ((ab, bd), False, aa, bb) \<in> kernel_call_conc e) \<or> ba = KernelPreempted \<and> bc = KernelSchedule True \<and> ((ab, bd), (), aa, bb) \<in> handle_preemption_conc \<or> (\<exists>b. ba = KernelSchedule b) \<and> bc = KernelExit \<and> ((ab, bd), (), aa, bb) \<in> schedule_conc \<or> ba = KernelExit \<and> ((ab, bd), bc, aa, bb) \<in> kernel_exit_conc \<or> ba = InUserMode \<and> (\<exists>a b e. bc = KernelEntry e \<and> ((ab, bd), None, a, b) \<in> check_active_irq_conc \<and> ((a, b), Some e, aa, bb) \<in> do_user_op_conc \<and> e \<noteq> Interrupt) \<or> ba = InUserMode \<and> bc = InUserMode \<and> (\<exists>a b. ((ab, bd), None, a, b) \<in> check_active_irq_conc \<and> ((a, b), None, aa, bb) \<in> do_user_op_conc) \<or> ba = InUserMode \<and> bc = KernelEntry Interrupt \<and> (\<exists>i. ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc) \<or> ba = InIdleMode \<and> bc = KernelEntry Interrupt \<and> (\<exists>i. ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc) \<or> ba = InIdleMode \<and> bc = InIdleMode \<and> ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab bd. ((\<exists>e. ba = KernelEntry e \<and> bc = KernelPreempted \<and> ((a, b), True, ab, bd) \<in> kernel_call_abs e \<and> e \<noteq> Interrupt) \<or> (\<exists>e. ba = KernelEntry e \<and> bc = KernelSchedule (e = Interrupt) \<and> ((a, b), False, ab, bd) \<in> kernel_call_abs e) \<or> ba = KernelPreempted \<and> bc = KernelSchedule True \<and> ((a, b), (), ab, bd) \<in> handle_preemption_abs \<or> (\<exists>b. ba = KernelSchedule b) \<and> bc = KernelExit \<and> ((a, b), (), ab, bd) \<in> schedule_abs \<or> ba = KernelExit \<and> ((a, b), bc, ab, bd) \<in> kernel_exit_abs \<or> ba = InUserMode \<and> (\<exists>aa ba e. bc = KernelEntry e \<and> ((a, b), None, aa, ba) \<in> check_active_irq_abs \<and> ((aa, ba), Some e, ab, bd) \<in> do_user_op_abs \<and> e \<noteq> Interrupt) \<or> ba = InUserMode \<and> bc = InUserMode \<and> (\<exists>aa ba. ((a, b), None, aa, ba) \<in> check_active_irq_abs \<and> ((aa, ba), None, ab, bd) \<in> do_user_op_abs) \<or> ba = InUserMode \<and> bc = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, ab, bd) \<in> check_active_irq_abs) \<or> ba = InIdleMode \<and> bc = KernelEntry Interrupt \<and> (\<exists>i. ((a, b), Some i, ab, bd) \<in> check_active_irq_abs) \<or> ba = InIdleMode \<and> bc = InIdleMode \<and> ((a, b), None, ab, bd) \<in> check_active_irq_abs) \<and> ((ab, bd), bc) \<in> extras_abs \<and> ((ab, bd), aa, bb) \<in> srel
 2. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<inter> invs_abs \<times> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (11 subgoals):
 1. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelEntry e) \<in> invs_abs; ((ab, bd), KernelEntry e) \<in> invs_conc; ba = KernelEntry e; bc = KernelPreempted; ((ab, bd), True, aa, bb) \<in> kernel_call_conc e; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), True, ab, ba) \<in> kernel_call_abs e \<and> ((ab, ba), KernelPreempted) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelEntry e) \<in> invs_abs; ((ab, bd), KernelEntry e) \<in> invs_conc; ba = KernelEntry e; bc = KernelSchedule (e = Interrupt); ((ab, bd), False, aa, bb) \<in> kernel_call_conc e\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), False, ab, ba) \<in> kernel_call_abs e \<and> ((ab, ba), KernelSchedule (e = Interrupt)) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelPreempted) \<in> invs_abs; ((ab, bd), KernelPreempted) \<in> invs_conc; ba = KernelPreempted; bc = KernelSchedule True; ((ab, bd), (), aa, bb) \<in> handle_preemption_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), (), ab, ba) \<in> handle_preemption_abs \<and> ((ab, ba), KernelSchedule True) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelSchedule be) \<in> invs_abs; ((ab, bd), KernelSchedule be) \<in> invs_conc; ba = KernelSchedule be; bc = KernelExit; ((ab, bd), (), aa, bb) \<in> schedule_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), (), ab, ba) \<in> schedule_abs \<and> ((ab, ba), KernelExit) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelExit) \<in> invs_abs; ((ab, bd), KernelExit) \<in> invs_conc; ba = KernelExit; ((ab, bd), bc, aa, bb) \<in> kernel_exit_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), bc, ab, ba) \<in> kernel_exit_abs \<and> ((ab, ba), bc) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>a b ba aa bb bc ab bd ac be e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry e; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 7. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 8. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 9. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 10. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelEntry e) \<in> invs_abs; ((ab, bd), KernelEntry e) \<in> invs_conc; ba = KernelEntry e; bc = KernelSchedule (e = Interrupt); ((ab, bd), False, aa, bb) \<in> kernel_call_conc e\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), False, ab, ba) \<in> kernel_call_abs e \<and> ((ab, ba), KernelSchedule (e = Interrupt)) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelPreempted) \<in> invs_abs; ((ab, bd), KernelPreempted) \<in> invs_conc; ba = KernelPreempted; bc = KernelSchedule True; ((ab, bd), (), aa, bb) \<in> handle_preemption_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), (), ab, ba) \<in> handle_preemption_abs \<and> ((ab, ba), KernelSchedule True) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelSchedule be) \<in> invs_abs; ((ab, bd), KernelSchedule be) \<in> invs_conc; ba = KernelSchedule be; bc = KernelExit; ((ab, bd), (), aa, bb) \<in> schedule_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), (), ab, ba) \<in> schedule_abs \<and> ((ab, ba), KernelExit) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelExit) \<in> invs_abs; ((ab, bd), KernelExit) \<in> invs_conc; ba = KernelExit; ((ab, bd), bc, aa, bb) \<in> kernel_exit_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), bc, ab, ba) \<in> kernel_exit_abs \<and> ((ab, ba), bc) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd ac be e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry e; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 7. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 8. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 9. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 10. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (9 subgoals):
 1. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelPreempted) \<in> invs_abs; ((ab, bd), KernelPreempted) \<in> invs_conc; ba = KernelPreempted; bc = KernelSchedule True; ((ab, bd), (), aa, bb) \<in> handle_preemption_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), (), ab, ba) \<in> handle_preemption_abs \<and> ((ab, ba), KernelSchedule True) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelSchedule be) \<in> invs_abs; ((ab, bd), KernelSchedule be) \<in> invs_conc; ba = KernelSchedule be; bc = KernelExit; ((ab, bd), (), aa, bb) \<in> schedule_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), (), ab, ba) \<in> schedule_abs \<and> ((ab, ba), KernelExit) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelExit) \<in> invs_abs; ((ab, bd), KernelExit) \<in> invs_conc; ba = KernelExit; ((ab, bd), bc, aa, bb) \<in> kernel_exit_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), bc, ab, ba) \<in> kernel_exit_abs \<and> ((ab, ba), bc) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd ac be e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry e; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 7. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 8. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 9. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (8 subgoals):
 1. \<And>a b ba aa bb bc ab bd be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelSchedule be) \<in> invs_abs; ((ab, bd), KernelSchedule be) \<in> invs_conc; ba = KernelSchedule be; bc = KernelExit; ((ab, bd), (), aa, bb) \<in> schedule_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), (), ab, ba) \<in> schedule_abs \<and> ((ab, ba), KernelExit) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelExit) \<in> invs_abs; ((ab, bd), KernelExit) \<in> invs_conc; ba = KernelExit; ((ab, bd), bc, aa, bb) \<in> kernel_exit_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), bc, ab, ba) \<in> kernel_exit_abs \<and> ((ab, ba), bc) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd ac be e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry e; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 7. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 8. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (7 subgoals):
 1. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), KernelExit) \<in> invs_abs; ((ab, bd), KernelExit) \<in> invs_conc; ba = KernelExit; ((ab, bd), bc, aa, bb) \<in> kernel_exit_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), bc, ab, ba) \<in> kernel_exit_abs \<and> ((ab, ba), bc) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd ac be e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry e; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 7. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb bc ab bd ac be e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry e; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb bc ab bd ac be e. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry e; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt; ((ac, be), InUserMode) \<in> invs_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (6 subgoals):
 1. \<And>a b aa bb ab bd ac be e ad bf. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt; ((ac, be), InUserMode) \<in> invs_conc; ((a, b), None, ad, bf) \<in> check_active_irq_abs; ((ad, bf), ac, be) \<in> srel; ((ad, bf), InUserMode) \<in> extras_abs\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (6 subgoals):
 1. \<And>a b aa bb ab bd ac be e ad bf. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), Some e, aa, bb) \<in> do_user_op_conc; e \<noteq> Interrupt; ((ac, be), InUserMode) \<in> invs_conc; ((a, b), None, ad, bf) \<in> check_active_irq_abs; ((ad, bf), ac, be) \<in> srel; ((ad, bf), InUserMode) \<in> extras_abs; ((ad, bf), InUserMode) \<in> invs_abs\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), Some e, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), KernelEntry e) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 6. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (5 subgoals):
 1. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (5 subgoals):
 1. \<And>a b ba aa bb bc ab bd ac be. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = InUserMode; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc; ((ac, be), InUserMode) \<in> invs_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (5 subgoals):
 1. \<And>a b aa bb ab bd ac be ad bf. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc; ((ac, be), InUserMode) \<in> invs_conc; ((a, b), None, ad, bf) \<in> check_active_irq_abs; ((ad, bf), ac, be) \<in> srel; ((ad, bf), InUserMode) \<in> extras_abs\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (5 subgoals):
 1. \<And>a b aa bb ab bd ac be ad bf. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ((ab, bd), None, ac, be) \<in> check_active_irq_conc; ((ac, be), None, aa, bb) \<in> do_user_op_conc; ((ac, be), InUserMode) \<in> invs_conc; ((a, b), None, ad, bf) \<in> check_active_irq_abs; ((ad, bf), ac, be) \<in> srel; ((ad, bf), InUserMode) \<in> extras_abs; ((ad, bf), InUserMode) \<in> invs_abs\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>aa bb. ((a, b), None, aa, bb) \<in> check_active_irq_abs \<and> ((aa, bb), None, ab, ba) \<in> do_user_op_abs) \<and> ((ab, ba), InUserMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 5. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (4 subgoals):
 1. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InUserMode) \<in> invs_abs; ((ab, bd), InUserMode) \<in> invs_conc; ba = InUserMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 4. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (3 subgoals):
 1. \<And>a b ba aa bb bc ab bd i. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = KernelEntry Interrupt; ((ab, bd), Some i, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. (\<exists>i. ((a, b), Some i, ab, ba) \<in> check_active_irq_abs) \<and> ((ab, ba), KernelEntry Interrupt) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 3. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc ab bd. \<lbrakk>((a, b), ab, bd) \<in> srel; ((a, b), InIdleMode) \<in> invs_abs; ((ab, bd), InIdleMode) \<in> invs_conc; ba = InIdleMode; bc = InIdleMode; ((ab, bd), None, aa, bb) \<in> check_active_irq_conc; ((aa, bb), InIdleMode) \<in> invs_conc\<rbrakk> \<Longrightarrow> \<exists>ab ba. ((a, b), None, ab, ba) \<in> check_active_irq_abs \<and> ((ab, ba), InIdleMode) \<in> extras_abs \<and> ((ab, ba), aa, bb) \<in> srel
 2. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc \<longrightarrow> Fin ADT_conc s' = Fin ADT_abs s proof (prove)
goal:
No subgoals!