theory ArchIpc_IF

lemma storeWord_equiv_but_for_labels[Ipc_IF_assms]:
  "\<lbrace>\<lambda>ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>) \<and>
         for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p\<rbrace>
   storeWord p v
   \<lbrace>\<lambda>_ ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>" unfolding storeWord_def apply (wp modify_wp) apply (clarsimp simp: equiv_but_for_labels_def) apply (rule states_equiv_forI) apply (fastforce intro!: equiv_forI elim!: states_equiv_forE dest: equiv_forD) apply (simp add: states_equiv_for_def) apply (rule conjI) apply (rule equiv_forI) apply clarsimp apply (drule_tac f=underlying_memory in equiv_forD,fastforce) apply (fastforce intro: is_aligned_no_wrap' word_plus_mono_right
                             simp: is_aligned_mask for_each_byte_of_word_def word_size_def) apply (rule equiv_forI) apply clarsimp apply (drule_tac f=device_state in equiv_forD,fastforce) apply clarsimp apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ekheap]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt_list]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=is_original_cap]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_states]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_irq_node]) apply (fastforce simp: equiv_asids_def equiv_asid_def elim: states_equiv_forE) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ready_queues]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>) \<and> for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p\<rbrace> storeWord p v \<lbrace>\<lambda>_ ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>) \<and> for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p\<rbrace> do assert (p && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! 1, p + 3 := word_rsplit v ! 0)))
od \<lbrace>\<lambda>_ ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. equiv_but_for_labels aag L st (s\<lparr>machine_state := sa\<rparr>) \<and> for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p \<Longrightarrow> p && mask 2 = 0 \<longrightarrow> equiv_but_for_labels aag L st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! 1, p + 3 := word_rsplit v ! 0)) sa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (10 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_machine_state (\<lambda>x. pasObjectAbs aag x \<notin> L) (machine_state st) (machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>))
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 10. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (9 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_machine_state (\<lambda>x. pasObjectAbs aag x \<notin> L) (machine_state st) (machine_state (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>))
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (9 subgoals):
 1. \<And>sa. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_machine_state (\<lambda>x. pasObjectAbs aag x \<notin> L) (machine_state st) (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (10 subgoals):
 1. \<And>sa. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa)
 2. \<And>sa. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 10. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (10 subgoals):
 1. \<And>sa x. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0; pasObjectAbs aag x \<notin> L\<rbrakk> \<Longrightarrow> underlying_memory (machine_state st) x = underlying_memory (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa) x
 2. \<And>sa. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 10. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (10 subgoals):
 1. \<And>sa x. \<lbrakk>cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0; pasObjectAbs aag x \<notin> L; equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa; equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa; equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>); equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>); equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>)\<rbrakk> \<Longrightarrow> (x = p \<longrightarrow> underlying_memory (machine_state st) p = word_rsplit v ! 3) \<and> (x \<noteq> p \<longrightarrow> (x = p + 1 \<longrightarrow> underlying_memory (machine_state st) (p + 1) = word_rsplit v ! 2) \<and> (x \<noteq> p + 1 \<longrightarrow> (x = p + 2 \<longrightarrow> underlying_memory (machine_state st) (p + 2) = word_rsplit v ! Suc 0) \<and> (x \<noteq> p + 2 \<longrightarrow> (x = p + 3 \<longrightarrow> underlying_memory (machine_state st) (p + 3) = word_rsplit v ! 0) \<and> (x \<noteq> p + 3 \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory sa x))))
 2. \<And>sa. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 10. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (10 subgoals):
 1. \<And>sa x. \<lbrakk>cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0; pasObjectAbs aag x \<notin> L; equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa; equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>); equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>); equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); underlying_memory (machine_state st) x = underlying_memory sa x\<rbrakk> \<Longrightarrow> (x = p \<longrightarrow> underlying_memory (machine_state st) p = word_rsplit v ! 3) \<and> (x \<noteq> p \<longrightarrow> (x = p + 1 \<longrightarrow> underlying_memory (machine_state st) (p + 1) = word_rsplit v ! 2) \<and> (x \<noteq> p + 1 \<longrightarrow> (x = p + 2 \<longrightarrow> underlying_memory (machine_state st) (p + 2) = word_rsplit v ! Suc 0) \<and> (x \<noteq> p + 2 \<longrightarrow> (x = p + 3 \<longrightarrow> underlying_memory (machine_state st) (p + 3) = word_rsplit v ! 0) \<and> (x \<noteq> p + 3 \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory sa x))))
 2. \<And>sa. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 10. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (9 subgoals):
 1. \<And>sa. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (9 subgoals):
 1. \<And>sa x. \<lbrakk>equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>) \<and> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0; pasObjectAbs aag x \<notin> L\<rbrakk> \<Longrightarrow> device_state (machine_state st) x = device_state (underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa) x
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (9 subgoals):
 1. \<And>sa x. \<lbrakk>cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0; pasObjectAbs aag x \<notin> L; equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa; equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) device_state (machine_state st) sa; equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>); equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>); equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>)\<rbrakk> \<Longrightarrow> device_state (machine_state st) x = device_state sa x
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (9 subgoals):
 1. \<And>sa x. \<lbrakk>cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0; pasObjectAbs aag x \<notin> L; equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) underlying_memory (machine_state st) sa; equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>); equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>); equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := sa\<rparr>); equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); device_state (machine_state st) x = device_state sa x\<rbrakk> \<Longrightarrow> device_state (machine_state st) x = device_state sa x
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 9. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (8 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 8. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (7 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 7. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 6. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 5. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 4. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 3. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>)
 2. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>machine_state := sa\<rparr>); cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) sa; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p; p && mask 2 = 0\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m a. if a = p + 3 then word_rsplit v ! 0 else if a = p + 2 then word_rsplit v ! Suc 0 else if a = p + 1 then word_rsplit v ! 2 else if a = p then word_rsplit v ! 3 else m a) sa\<rparr>) proof (prove)
goal:
No subgoals!