theory Noninterference

lemma sameFor_subject_def2:
  "sameFor_subject g ab irqab asidab domainab l =
     {(os,os') | os os' s s'. s = internal_state_if os \<and> s' = internal_state_if os' \<and>
                 (\<forall>d \<in> subjectReads g (OrdinaryLabel l).
                    states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x  = d)
                                     (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) s s') \<and>
                 ((domainab (cur_domain s) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {} \<or>
                   domainab (cur_domain s') \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {})
                  \<longrightarrow> cur_domain s = cur_domain s' \<and> globals_equiv s s' \<and>
                      scheduler_action s = scheduler_action s' \<and>
                      work_units_completed s = work_units_completed s' \<and>
                      irq_state (machine_state s) = irq_state (machine_state s') \<and>
                      (user_modes (sys_mode_of os) \<longrightarrow> user_context_of os = user_context_of os') \<and>
                      sys_mode_of os = sys_mode_of os' \<and>
                      equiv_for (\<lambda>x. ab x = SilcLabel) kheap s s')}" apply (clarsimp simp: sameFor_subject_def) apply (rule equalityI) apply (rule subsetI) apply (drule CollectD) apply (rule CollectI) apply (clarify) apply (rule exI)+ apply (rule conjI, rule refl) apply (rule conjI) apply (rule ballI) apply (erule states_equiv_for_guard_imp) apply (blast+)[4] apply (fastforce simp: globals_equiv_def) apply (rule subsetI) apply (drule CollectD) apply (rule CollectI) apply (clarify) apply (rule exI)+ apply (rule conjI, rule refl) apply (rule conjI) apply (rule states_equiv_forI) apply ((fastforce intro: equiv_forI elim: states_equiv_forE equiv_forD)+)[5] apply (fastforce intro: equiv_forI elim: states_equiv_forE_is_original_cap) apply ((fastforce intro: equiv_forI elim: states_equiv_forE equiv_forD)+)[2] apply (solves \<open>clarsimp simp: equiv_asids_def states_equiv_for_def\<close>) apply (fastforce intro: equiv_forI elim: states_equiv_forE_ready_queues) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sameFor_subject g ab irqab asidab domainab l = {uu_. \<exists>os os' s s'. uu_ = (os, os') \<and> s = internal_state_if os \<and> s' = internal_state_if os' \<and> (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) s s') \<and> (domainab (cur_domain s) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {} \<or> domainab (cur_domain s') \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {} \<longrightarrow> cur_domain s = cur_domain s' \<and> globals_equiv s s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') \<and> (user_modes (sys_mode_of os) \<longrightarrow> user_context_of os = user_context_of os') \<and> sys_mode_of os = sys_mode_of os' \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap s s')} proof (prove)
goal (1 subgoal):
 1. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} = {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (2 subgoals):
 1. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)}
 2. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<Longrightarrow> x \<in> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)}
 2. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>a b ba aa bb bc. x = (((a, b), ba), (aa, bb), bc) \<and> states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb) \<Longrightarrow> x \<in> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)}
 2. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>a b ba aa bb bc. x = (((a, b), ba), (aa, bb), bc) \<and> states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb) \<Longrightarrow> \<exists>a b ba aa bb bc. x = (((a, b), ba), (aa, bb), bc) \<and> (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)
 2. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> \<exists>a b ba aa bb bc. (((aba, bd), be), (ac, bf), bg) = (((a, b), ba), (aa, bb), bc) \<and> (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)
 2. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (((aba, bd), be), (ac, bf), bg) = (((?a50 a b ba aa bb bc aba bd be ac bf bg, ?b52 a b ba aa bb bc aba bd be ac bf bg), ?b54 a b ba aa bb bc aba bd be ac bf bg), (?a56 a b ba aa bb bc aba bd be ac bf bg, ?b58 a b ba aa bb bc aba bd be ac bf bg), ?b60 a b ba aa bb bc aba bd be ac bf bg) \<and> (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) (?b52 a b ba aa bb bc aba bd be ac bf bg) (?b58 a b ba aa bb bc aba bd be ac bf bg)) \<and> ((domainab (cur_domain (?b52 a b ba aa bb bc aba bd be ac bf bg)) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain (?b58 a b ba aa bb bc aba bd be ac bf bg)) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain (?b52 a b ba aa bb bc aba bd be ac bf bg) = cur_domain (?b58 a b ba aa bb bc aba bd be ac bf bg) \<and> globals_equiv (?b52 a b ba aa bb bc aba bd be ac bf bg) (?b58 a b ba aa bb bc aba bd be ac bf bg) \<and> scheduler_action (?b52 a b ba aa bb bc aba bd be ac bf bg) = scheduler_action (?b58 a b ba aa bb bc aba bd be ac bf bg) \<and> work_units_completed (?b52 a b ba aa bb bc aba bd be ac bf bg) = work_units_completed (?b58 a b ba aa bb bc aba bd be ac bf bg) \<and> equiv_irq_state (machine_state (?b52 a b ba aa bb bc aba bd be ac bf bg)) (machine_state (?b58 a b ba aa bb bc aba bd be ac bf bg)) \<and> (user_modes (?b54 a b ba aa bb bc aba bd be ac bf bg) \<longrightarrow> ?a50 a b ba aa bb bc aba bd be ac bf bg = ?a56 a b ba aa bb bc aba bd be ac bf bg) \<and> ?b54 a b ba aa bb bc aba bd be ac bf bg = ?b60 a b ba aa bb bc aba bd be ac bf bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap (?b52 a b ba aa bb bc aba bd be ac bf bg) (?b58 a b ba aa bb bc aba bd be ac bf bg))
 2. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf) \<and> ((domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf)
 2. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (3 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> \<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf
 2. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf
 3. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (3 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg d. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf; d \<in> subjectReads g (OrdinaryLabel l)\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf
 2. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf
 3. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg d x. \<lbrakk>(domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf; d \<in> subjectReads g (OrdinaryLabel l); ab x = d\<rbrakk> \<Longrightarrow> ab x \<in> subjectReads g (OrdinaryLabel l)
 2. \<And>a b ba aa bb bc aba bd be ac bf bg d x. \<lbrakk>(domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf; d \<in> subjectReads g (OrdinaryLabel l); irqab x = d\<rbrakk> \<Longrightarrow> irqab x \<in> subjectReads g (OrdinaryLabel l)
 3. \<And>a b ba aa bb bc aba bd be ac bf bg d x. \<lbrakk>(domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf; d \<in> subjectReads g (OrdinaryLabel l); asidab x = d\<rbrakk> \<Longrightarrow> asidab x \<in> subjectReads g (OrdinaryLabel l)
 4. \<And>a b ba aa bb bc aba bd be ac bf bg d x. \<lbrakk>(domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf; d \<in> subjectReads g (OrdinaryLabel l); d \<in> domainab x\<rbrakk> \<Longrightarrow> domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}
 5. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf
 6. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf
 2. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (1 subgoal):
 1. {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<subseteq> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} \<Longrightarrow> x \<in> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>a b ba aa bb bc. x = (((a, b), ba), (aa, bb), bc) \<and> (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb) \<Longrightarrow> x \<in> {(((a, b), ba), (aa, bb), bc) |a b ba aa bb bc. states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb)} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>a b ba aa bb bc. x = (((a, b), ba), (aa, bb), bc) \<and> (\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) b bb) \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb) \<Longrightarrow> \<exists>a b ba aa bb bc. x = (((a, b), ba), (aa, bb), bc) \<and> states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> \<exists>a b ba aa bb bc. (((aba, bd), be), (ac, bf), bg) = (((a, b), ba), (aa, bb), bc) \<and> states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) b bb \<and> ((domainab (cur_domain b) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bb) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap b bb) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (((aba, bd), be), (ac, bf), bg) = (((?a522 a b ba aa bb bc aba bd be ac bf bg, ?b524 a b ba aa bb bc aba bd be ac bf bg), ?b526 a b ba aa bb bc aba bd be ac bf bg), (?a528 a b ba aa bb bc aba bd be ac bf bg, ?b530 a b ba aa bb bc aba bd be ac bf bg), ?b532 a b ba aa bb bc aba bd be ac bf bg) \<and> states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) (?b524 a b ba aa bb bc aba bd be ac bf bg) (?b530 a b ba aa bb bc aba bd be ac bf bg) \<and> ((domainab (cur_domain (?b524 a b ba aa bb bc aba bd be ac bf bg)) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain (?b530 a b ba aa bb bc aba bd be ac bf bg)) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain (?b524 a b ba aa bb bc aba bd be ac bf bg) = cur_domain (?b530 a b ba aa bb bc aba bd be ac bf bg) \<and> globals_equiv (?b524 a b ba aa bb bc aba bd be ac bf bg) (?b530 a b ba aa bb bc aba bd be ac bf bg) \<and> scheduler_action (?b524 a b ba aa bb bc aba bd be ac bf bg) = scheduler_action (?b530 a b ba aa bb bc aba bd be ac bf bg) \<and> work_units_completed (?b524 a b ba aa bb bc aba bd be ac bf bg) = work_units_completed (?b530 a b ba aa bb bc aba bd be ac bf bg) \<and> equiv_irq_state (machine_state (?b524 a b ba aa bb bc aba bd be ac bf bg)) (machine_state (?b530 a b ba aa bb bc aba bd be ac bf bg)) \<and> (user_modes (?b526 a b ba aa bb bc aba bd be ac bf bg) \<longrightarrow> ?a522 a b ba aa bb bc aba bd be ac bf bg = ?a528 a b ba aa bb bc aba bd be ac bf bg) \<and> ?b526 a b ba aa bb bc aba bd be ac bf bg = ?b532 a b ba aa bb bc aba bd be ac bf bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap (?b524 a b ba aa bb bc aba bd be ac bf bg) (?b530 a b ba aa bb bc aba bd be ac bf bg)) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf \<and> ((domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) bd bf
 2. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf proof (prove)
goal (11 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) kheap bd bf
 2. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_machine_state (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) (machine_state bd) (machine_state bf)
 3. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) \<circ> fst) cdt bd bf
 4. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) ekheap bd bf
 5. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) \<circ> fst) cdt_list bd bf
 6. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) \<circ> fst) is_original_cap bd bf
 7. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) interrupt_states bd bf
 8. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) interrupt_irq_node bd bf
 9. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) bd bf
 10. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) ready_queues bd bf
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. ab x \<in> subjectReads g (OrdinaryLabel l)) \<circ> fst) is_original_cap bd bf
 2. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) interrupt_states bd bf
 3. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) interrupt_irq_node bd bf
 4. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) bd bf
 5. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) ready_queues bd bf
 6. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf proof (prove)
goal (5 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) interrupt_states bd bf
 2. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. irqab x \<in> subjectReads g (OrdinaryLabel l)) interrupt_irq_node bd bf
 3. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) bd bf
 4. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) ready_queues bd bf
 5. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf proof (prove)
goal (3 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. asidab x \<in> subjectReads g (OrdinaryLabel l)) bd bf
 2. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) ready_queues bd bf
 3. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. domainab x \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) ready_queues bd bf
 2. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc aba bd be ac bf bg. \<lbrakk>\<forall>d\<in>subjectReads g (OrdinaryLabel l). states_equiv_for (\<lambda>x. ab x = d) (\<lambda>x. irqab x = d) (\<lambda>x. asidab x = d) (\<lambda>x. d \<in> domainab x) bd bf; (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf\<rbrakk> \<Longrightarrow> (domainab (cur_domain bd) \<inter> subjectReads g (OrdinaryLabel l) = {} \<longrightarrow> domainab (cur_domain bf) \<inter> subjectReads g (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain bd = cur_domain bf \<and> globals_equiv bd bf \<and> scheduler_action bd = scheduler_action bf \<and> work_units_completed bd = work_units_completed bf \<and> equiv_irq_state (machine_state bd) (machine_state bf) \<and> (user_modes be \<longrightarrow> aba = ac) \<and> be = bg \<and> equiv_for (\<lambda>x. ab x = SilcLabel) kheap bd bf proof (prove)
goal:
No subgoals!