theory ArchNoninterference

lemma ev2_invisible'[Noninterference_assms]:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "\<lbrakk> labels_are_invisible aag l L; labels_are_invisible aag l L';
       modifies_at_most aag L Q f; modifies_at_most aag L' Q' g;
       doesnt_touch_globals Q f; doesnt_touch_globals Q' g;
       \<And>st :: det_state. f \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>;
       \<And>st :: det_state. g \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>;
       \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>(rva,s') \<in> fst (f s). \<forall>(rvb,t') \<in> fst (g t). W rva rvb) \<rbrakk>
       \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag)
                         (\<lambda>s s'. affects_equiv aag l s s' \<and>
                                 arch_globals_equiv_strengthener (machine_state s) (machine_state s'))
                         (\<lambda>s s'. affects_equiv aag l s s' \<and>
                                 arch_globals_equiv_strengthener (machine_state s) (machine_state s'))
                         W (P and Q) (P' and Q') f g" apply (clarsimp simp: equiv_valid_2_def) apply (rule conjI) apply blast apply (drule_tac s=s in modifies_at_mostD, assumption+) apply (drule_tac s=t in modifies_at_mostD, assumption+) apply (drule_tac s=s in globals_equivI, assumption+) apply (drule_tac s=t in globals_equivI, assumption+) apply (frule (1) equiv_but_for_reads_equiv[OF domains_distinct]) apply (frule_tac s=t in equiv_but_for_reads_equiv[OF domains_distinct], assumption) apply (drule (1) equiv_but_for_affects_equiv[OF domains_distinct]) apply (drule_tac s=t in equiv_but_for_affects_equiv[OF domains_distinct], assumption) apply (clarsimp simp: reads_equiv_g_def) apply (simp only: conj_assoc[symmetric]) apply (rule conjI) apply (blast intro: reads_equiv_trans reads_equiv_sym affects_equiv_trans
                       affects_equiv_sym globals_equiv_trans globals_equiv_sym) apply atomize apply (erule_tac x=s in allE) apply (erule_tac x=t in allE) apply (clarsimp simp: valid_def) apply (thin_tac "\<forall>x y. P x y" for P) apply (erule_tac x=s in allE) apply (erule_tac x=t in allE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; doesnt_touch_globals Q f; doesnt_touch_globals Q' g; \<And>st. \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (g t). W rva rvb)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) W (P and Q) (P' and Q') f g proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; doesnt_touch_globals Q f; doesnt_touch_globals Q' g; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t)\<rbrakk> \<Longrightarrow> W a aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; doesnt_touch_globals Q f; doesnt_touch_globals Q' g; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t)\<rbrakk> \<Longrightarrow> W a aa
 2. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; doesnt_touch_globals Q f; doesnt_touch_globals Q' g; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t)\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; doesnt_touch_globals Q f; doesnt_touch_globals Q' g; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t)\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L' Q' g; doesnt_touch_globals Q f; doesnt_touch_globals Q' g; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; doesnt_touch_globals Q f; doesnt_touch_globals Q' g; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; doesnt_touch_globals Q' g; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L'; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv_g aag s t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> globals_equiv b ba \<and> affects_equiv aag l b ba \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t\<rbrakk> \<Longrightarrow> ((reads_equiv aag b ba \<and> globals_equiv b ba) \<and> affects_equiv aag l b ba) \<and> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>\<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t\<rbrakk> \<Longrightarrow> (reads_equiv aag b ba \<and> globals_equiv b ba) \<and> affects_equiv aag l b ba
 2. \<And>s t a b aa ba. \<lbrakk>\<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<And>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> f \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>st. \<lbrace>\<lambda>s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state st) = exclusive_state (machine_state s)\<rbrace>; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t; \<lbrace>\<lambda>sa. exclusive_state (machine_state s) = exclusive_state (machine_state sa)\<rbrace> f \<lbrace>\<lambda>_ sa. exclusive_state (machine_state s) = exclusive_state (machine_state sa)\<rbrace>\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t; \<lbrace>\<lambda>sa. exclusive_state (machine_state s) = exclusive_state (machine_state sa)\<rbrace> f \<lbrace>\<lambda>_ sa. exclusive_state (machine_state s) = exclusive_state (machine_state sa)\<rbrace>; \<lbrace>\<lambda>s. exclusive_state (machine_state t) = exclusive_state (machine_state s)\<rbrace> g \<lbrace>\<lambda>_ s. exclusive_state (machine_state t) = exclusive_state (machine_state s)\<rbrace>\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t; \<forall>s. exclusive_state (machine_state t) = exclusive_state (machine_state s) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s')); \<forall>s. exclusive_state (machine_state t) = exclusive_state (machine_state s) \<longrightarrow> (\<forall>x\<in>fst (g s). case x of (r, s') \<Rightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'))\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state 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 (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t; \<forall>s. exclusive_state (machine_state t) = exclusive_state (machine_state s) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s')); \<forall>s. exclusive_state (machine_state t) = exclusive_state (machine_state s) \<longrightarrow> (\<forall>x\<in>fst (g s). case x of (r, s') \<Rightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'))\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state 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 (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t; \<forall>s. exclusive_state (machine_state t) = exclusive_state (machine_state s) \<longrightarrow> (\<forall>x\<in>fst (g s). case x of (r, s') \<Rightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s')); exclusive_state (machine_state t) = exclusive_state (machine_state s) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'))\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state 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 (g t); P s; Q s; P' t; Q' t; affects_equiv aag l s t; exclusive_state (machine_state s) = exclusive_state (machine_state t); equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; globals_equiv s b; globals_equiv t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba; reads_equiv aag s t; globals_equiv s t; exclusive_state (machine_state t) = exclusive_state (machine_state s) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s')); exclusive_state (machine_state t) = exclusive_state (machine_state t) \<longrightarrow> (\<forall>x\<in>fst (g t). case x of (r, s') \<Rightarrow> exclusive_state (machine_state t) = exclusive_state (machine_state s'))\<rbrakk> \<Longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state ba) proof (prove)
goal:
No subgoals!