theory Arch_IF

lemma equiv_valid_2_unobservable:
  assumes f:
    "\<And>P Q R S st. \<lbrace>states_equiv_for P Q R S st\<rbrace> f \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>"
  assumes f':
    "\<And>P Q R S st. \<lbrace>states_equiv_for P Q R S st\<rbrace> f' \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>"
  assumes g:
    "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
  assumes g':
    "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f' \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
  assumes h:
    "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>"
  assumes h':
    "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f' \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>"
  assumes j:
    "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
  assumes j':
    "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f' \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
  assumes k:
    "\<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> f \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>"
  assumes k':
    "\<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> f' \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>"
  assumes l:
    "\<And>P. \<lbrace>\<lambda>s. P (irq_state (machine_state s))\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_state (machine_state s))\<rbrace>"
  assumes l':
    "\<And>P. \<lbrace>\<lambda>s. P (irq_state (machine_state s))\<rbrace> f' \<lbrace>\<lambda>rv s. P (irq_state (machine_state s))\<rbrace>"
  shows
    "equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) \<top>\<top> \<top> \<top> f f'" apply (clarsimp simp: equiv_valid_2_def) apply (frule use_valid[OF _ f]) apply (rule states_equiv_for_refl) apply (frule use_valid[OF _ f']) apply (rule states_equiv_for_refl) apply (frule use_valid[OF _ f]) apply (rule states_equiv_for_refl) apply (frule use_valid[OF _ f']) apply (rule states_equiv_for_refl) apply (frule use_valid) apply (rule_tac P="(=) (cur_thread s)" in g) apply (rule refl) apply (frule_tac f=f' in use_valid) apply (rule_tac P="(=) (cur_thread t)" in g') apply (rule refl) apply (frule use_valid) apply (rule_tac P="(=) (cur_domain s)" in h) apply (rule refl) apply (frule_tac f=f' in use_valid) apply (rule_tac P="(=) (cur_domain t)" in h') apply (rule refl) apply (frule use_valid) apply (rule_tac P="(=) (scheduler_action s)" in j) apply (rule refl) apply (frule_tac f=f' in use_valid) apply (rule_tac P="(=) (scheduler_action t)" in j') apply (rule refl) apply (frule use_valid) apply (rule_tac P="(=) (work_units_completed s)" in k) apply (rule refl) apply (frule_tac f=f' in use_valid) apply (rule_tac P="(=) (work_units_completed t)" in k') apply (rule refl) apply (frule use_valid) apply (rule_tac P="(=) (irq_state (machine_state s))" in l) apply (rule refl) apply (frule_tac f=f' in use_valid) apply (rule_tac P="(=) (irq_state (machine_state t))" in l') apply (rule refl) apply (clarsimp simp: reads_equiv_def2 affects_equiv_def2) apply (auto intro: states_equiv_for_sym states_equiv_for_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (\<lambda>_. True) (\<lambda>_. True) f f' proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) (?st19 s t a b aa ba) s
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) (?st19 s t a b aa ba) b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b\<rbrakk> \<Longrightarrow> states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) (?st23 s t a b aa ba) t
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) (?st23 s t a b aa ba) ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba\<rbrakk> \<Longrightarrow> states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) (?st27 s t a b aa ba) s
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) (?st27 s t a b aa ba) b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b\<rbrakk> \<Longrightarrow> states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) (?st31 s t a b aa ba) t
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) (?st31 s t a b aa ba) ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba\<rbrakk> \<Longrightarrow> \<lbrace>?P35 s t a b aa ba\<rbrace> f \<lbrace>?Q35 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba\<rbrakk> \<Longrightarrow> ?P35 s t a b aa ba s
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; ?Q35 s t a b aa ba a b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b\<rbrakk> \<Longrightarrow> \<lbrace>?P40 s t a b aa ba\<rbrace> f' \<lbrace>?Q40 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b\<rbrakk> \<Longrightarrow> ?P40 s t a b aa ba t
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; ?Q40 s t a b aa ba aa ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b\<rbrakk> \<Longrightarrow> cur_thread t = cur_thread t
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba\<rbrakk> \<Longrightarrow> \<lbrace>?P43 s t a b aa ba\<rbrace> f \<lbrace>?Q43 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba\<rbrakk> \<Longrightarrow> ?P43 s t a b aa ba s
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; ?Q43 s t a b aa ba a b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba\<rbrakk> \<Longrightarrow> cur_domain s = cur_domain s
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b\<rbrakk> \<Longrightarrow> \<lbrace>?P48 s t a b aa ba\<rbrace> f' \<lbrace>?Q48 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b\<rbrakk> \<Longrightarrow> ?P48 s t a b aa ba t
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; ?Q48 s t a b aa ba aa ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b\<rbrakk> \<Longrightarrow> cur_domain t = cur_domain t
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba\<rbrakk> \<Longrightarrow> \<lbrace>?P51 s t a b aa ba\<rbrace> f \<lbrace>?Q51 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba\<rbrakk> \<Longrightarrow> ?P51 s t a b aa ba s
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; ?Q51 s t a b aa ba a b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba\<rbrakk> \<Longrightarrow> scheduler_action s = scheduler_action s
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b\<rbrakk> \<Longrightarrow> \<lbrace>?P56 s t a b aa ba\<rbrace> f' \<lbrace>?Q56 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b\<rbrakk> \<Longrightarrow> ?P56 s t a b aa ba t
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; ?Q56 s t a b aa ba aa ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b\<rbrakk> \<Longrightarrow> scheduler_action t = scheduler_action t
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba\<rbrakk> \<Longrightarrow> \<lbrace>?P59 s t a b aa ba\<rbrace> f \<lbrace>?Q59 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba\<rbrakk> \<Longrightarrow> ?P59 s t a b aa ba s
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; ?Q59 s t a b aa ba a b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba\<rbrakk> \<Longrightarrow> work_units_completed s = work_units_completed s
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b\<rbrakk> \<Longrightarrow> \<lbrace>?P64 s t a b aa ba\<rbrace> f' \<lbrace>?Q64 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b\<rbrakk> \<Longrightarrow> ?P64 s t a b aa ba t
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; ?Q64 s t a b aa ba aa ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b\<rbrakk> \<Longrightarrow> work_units_completed t = work_units_completed t
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba\<rbrakk> \<Longrightarrow> \<lbrace>?P67 s t a b aa ba\<rbrace> f \<lbrace>?Q67 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba\<rbrakk> \<Longrightarrow> ?P67 s t a b aa ba s
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; ?Q67 s t a b aa ba a b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba\<rbrakk> \<Longrightarrow> equiv_irq_state (machine_state s) (machine_state s)
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state b)\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state b)\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state b)\<rbrakk> \<Longrightarrow> \<lbrace>?P72 s t a b aa ba\<rbrace> f' \<lbrace>?Q72 s t a b aa ba\<rbrace>
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state b)\<rbrakk> \<Longrightarrow> ?P72 s t a b aa ba t
 3. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state b); ?Q72 s t a b aa ba aa ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state b)\<rbrakk> \<Longrightarrow> equiv_irq_state (machine_state t) (machine_state t)
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state b); equiv_irq_state (machine_state t) (machine_state ba)\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); reads_equiv aag s t; affects_equiv aag l s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread b; cur_thread t = cur_thread ba; cur_domain s = cur_domain b; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action b; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed b; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state b); equiv_irq_state (machine_state t) (machine_state ba)\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) s t; states_equiv_for (?P19 s t a b aa ba) (?Q19 s t a b aa ba) (?R19 s t a b aa ba) (?S19 s t a b aa ba) s b; states_equiv_for (?P23 s t a b aa ba) (?Q23 s t a b aa ba) (?R23 s t a b aa ba) (?S23 s t a b aa ba) t ba; states_equiv_for (?P27 s t a b aa ba) (?Q27 s t a b aa ba) (?R27 s t a b aa ba) (?S27 s t a b aa ba) s b; states_equiv_for (?P31 s t a b aa ba) (?Q31 s t a b aa ba) (?R31 s t a b aa ba) (?S31 s t a b aa ba) t ba; cur_thread s = cur_thread ba; cur_thread t = cur_thread ba; cur_domain s = cur_domain ba; cur_domain t = cur_domain ba; scheduler_action s = scheduler_action ba; scheduler_action t = scheduler_action ba; work_units_completed s = work_units_completed ba; work_units_completed t = work_units_completed ba; equiv_irq_state (machine_state s) (machine_state ba); equiv_irq_state (machine_state t) (machine_state ba); states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s t; cur_thread b = cur_thread ba; cur_domain b = cur_domain ba; scheduler_action b = scheduler_action ba; work_units_completed b = work_units_completed ba; equiv_irq_state (machine_state b) (machine_state ba)\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) b ba \<and> states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) b ba proof (prove)
goal:
No subgoals!